Products induces topology on fibers

Stream: new members

[Nicolò Cavalleri]

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]

One direction is going to be continuity of prod.mk

[Mario Carneiro]

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]

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]

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]

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]

Ok thanks. Is the name constant_induces_top appropriate?

[Nicolò Cavalleri]

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]

id isn't reducible so there is no surprise here

[Reid Barton]

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]

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

[Reid Barton]

I don't really think any action is needed

[Reid Barton]

You could finish with exact induced_id.symm

[Reid Barton]

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]

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