Zulip Chat Archive

Stream: general

Topic: why did this work?

Koundinya Vajjha (May 15 2019 at 18:54):

I just ran into this and was confused about why it worked:

import measure_theory.borel_space

universe u

open measure_theory

variables {α β: Type u}

instance fn_space.measurable_space [m₁ : measurable_space α] [m₂ : measurable_space β] [ topological_space α] [topological_space β] :
measurable_space (α  β) :=
borel (α  β)

If I remove the topological_space instances, Lean complains that it doesn't know how to find an instance of topological_space (α → β). So if I leave them on, somehow it is finding that instance on its own. Is this because of the compact_open topology? (But isn't that only for the subtype of continuous functions from(α → β)?

Koundinya Vajjha (May 15 2019 at 19:02):

Ah. set_option trace.class_instances true says that Pi.topological_space is the culprit.

Kevin Buzzard (May 15 2019 at 19:36):

Right. A -> B can be regarded as a product of B's over A, so for lots of structures (groups, topological spaces etc) A -> B inherits a structure from B. For topological groups this results in a gotcha -- asking that G -> G -> G is continuous makes sense but is not what you want, you lose the topology on the middle G.

Koundinya Vajjha (May 15 2019 at 20:55):

Also related: why is Lean happy with this?

instance set.measurable_space [m : measurable_space α] : measurable_space (set α) := 

Koundinya Vajjha (May 15 2019 at 20:56):

Even works. I'm very confused.

Chris Hughes (May 15 2019 at 21:28):

I don't know what a measurable space is, but I guess measurable_space is a lattice, and top is probably the space where every set has infinite measure or something like that.

Kenny Lau (May 15 2019 at 21:29):

unlike what its name suggests, measurable spaces don't actually need a measure

Kenny Lau (May 15 2019 at 21:30):

it's just a sigma algebra

Chris Hughes (May 15 2019 at 21:34):

That's why they're measurable and not measured.

Koundinya Vajjha (May 15 2019 at 21:37):

Yes it's just the sigma algebra. So why does top do it? I was expecting something like the powerset of alpha.

Kenny Lau (May 15 2019 at 21:38):

yes it is the powerset

Koundinya Vajjha (May 15 2019 at 21:39):

Oooh the powerset is top for the lattice of set inclusions?

Kenny Lau (May 15 2019 at 21:40):


Reid Barton (May 15 2019 at 23:00):

Incidentally the topology on a -> b doesn't depend on the topology on a at all, which I guess is the most natural choice if you really consider all functions. So topological_space a isn't contributing anything in your original example.

Last updated: Dec 20 2023 at 11:08 UTC