why did this work?

Stream: general

[Koundinya Vajjha]

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]

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

[Kevin Buzzard]

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]

Also related: why is Lean happy with this?

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

[Koundinya Vajjha]

Even ⊥ works. I'm very confused.

[Chris Hughes]

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]

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

[Kenny Lau]

it's just a sigma algebra

[Chris Hughes]

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

[Koundinya Vajjha]

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

[Kenny Lau]

yes it is the powerset

[Koundinya Vajjha]

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

[Kenny Lau]

right

[Reid Barton]

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.