# 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):

right

#### 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