## Stream: new members

### Topic: Products induces topology on fibers

#### Nicolò Cavalleri (Dec 20 2020 at 10:58):

I got a bit rusty: how do I prove something like this (supposing it says what I want to say)

example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] :
∀ x : X, inducing (λ y : Y, prod.mk x y) := sorry


?

#### Mario Carneiro (Dec 20 2020 at 11:24):

One direction is going to be continuity of prod.mk

#### Mario Carneiro (Dec 20 2020 at 11:33):

example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y]
(x : X) : inducing (λ y : Y, prod.mk x y) :=
begin
refine ⟨le_antisymm (continuous_const.prod_mk continuous_id).le_induced (λ s h, _)⟩,
convert is_open_induced (is_open_univ.prod h),
ext x, simp
end


#### Nicolò Cavalleri (Dec 20 2020 at 11:51):

Ok thanks! I was trying this way:

lemma constant_induces_top {X : Type*} {Y : Type*} [t : topological_space X] {x : X} :
t.induced (λ y : Y, x) = ⊤ := by { sorry, }

example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] :
∀ x : X, inducing (λ y : Y, prod.mk x y) := λ z,
⟨by {rw prod.topological_space,
simp only [induced_inf, induced_compose, function.comp, constant_induces_top, top_inf_eq],
rw [induced_id], }⟩


but the last rw does not work... do you know why? (I missed a bit when I first pasted it, sorry)

#### Nicolò Cavalleri (Dec 20 2020 at 12:37):

Also what is a smart way to prove

lemma constant_induces_top {X : Type*} {Y : Type*} [t : topological_space X] {x : X} :
t.induced (λ y : Y, x) = ⊤ := sorry


without going back to definitions?

#### Reid Barton (Dec 20 2020 at 12:40):

It's equivalent to the statement with >=, which is equivalent to λ y : Y, x being continuous w.r.t. ⊤ (or any topology), which is continuous_const

#### Nicolò Cavalleri (Dec 20 2020 at 13:04):

Ok thanks. Is the name constant_induces_top appropriate?

#### Nicolò Cavalleri (Dec 20 2020 at 13:06):

Also my proof above works if I add this lemma

lemma induced_id' {α : Type*} [t : topological_space α] : t.induced (λ a : α, a) = t := induced_id


What should I do? Should this new lemma go into mathlib or should I report that id is not working properly?

#### Reid Barton (Dec 20 2020 at 13:11):

id isn't reducible so there is no surprise here

#### Reid Barton (Dec 20 2020 at 13:13):

Nicolò Cavalleri said:

Ok thanks. Is the name constant_induces_top appropriate?

I think we would call it something more like induced_const

#### Nicolò Cavalleri (Dec 20 2020 at 13:13):

Ok should we change the statement of induced_id? Or what solution do you propose?

#### Reid Barton (Dec 20 2020 at 13:15):

I don't really think any action is needed

#### Reid Barton (Dec 20 2020 at 13:15):

You could finish with exact induced_id.symm

#### Reid Barton (Dec 20 2020 at 13:16):

Certainly adding a lemma would be better than changing an existing lemma, but I'm not sure if it will ever see real use

#### Reid Barton (Dec 20 2020 at 13:19):

I'm not really sure if there is a reason that function.comp is reducible but not id... it is a bit confusing

Last updated: May 17 2021 at 22:15 UTC