continuous_lift_prod_right — Mathlib

English

If f is a quotient map and hg is continuous on Y × X0 via hg(p.1, f p.2), then g is continuous.

Русский

Пусть f — тождественная карта и hg непрерывна на Y × X0 через hg(p.1, f p.2); тогда g непрерывна.

LaTeX

$$$(\\text{hf} : IsQuotientMap f) \\Rightarrow (\\text{Continuous}(p \\mapsto g(p.1, f p.2)) \\Rightarrow \\text{Continuous } g)$$$

Lean4

theorem continuous_lift_prod_right (hf : IsQuotientMap f) {g : Y × X → Z}
    (hg : Continuous fun p : Y × X₀ => g (p.1, f p.2)) : Continuous g :=
  by
  have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) := hg.comp continuous_swap
  have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
  exact (hf.continuous_lift_prod_left this).comp continuous_swap

Похожие утверждения