TopologicalSpace.prod_mono

Stream: Is there code for X?

[Kevin Buzzard]

We have docs#Set.prod_mono and docs#Filter.prod_mono but I couldn 't find

import Mathlib

theorem TopologicalSpace.prod_mono {α β : Type*} {σ₁ σ₂ : TopologicalSpace α}
    {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) :
    @instTopologicalSpaceProd α β σ₁ τ₁ ≤ @instTopologicalSpaceProd α β σ₂ τ₂ :=
  le_inf (le_trans inf_le_left <| induced_mono hσ)
         (le_trans inf_le_right <| induced_mono hτ)

Is this missing for some reason to do with instances, did I miss it, should I PR?

[Yury G. Kudryashov]

It's continuity of Prod.map in disguise

[Yury G. Kudryashov]

I think that we rarely have mono lemmas for type classes

[Yury G. Kudryashov]

Do you really need multiple topologies on the same type?

[Kevin Buzzard]

See my recent mathoverflow question for the continuation of the action topology story

[Kevin Buzzard]

I'm writing the API for version 5 of the topology on a module