quotient_lift — Mathlib

English

Let f: X → Y be continuous and compatible with the quotient relation at the level of quotients. Then Quotient.lift f hs: Quotient s → Y is continuous.

Русский

Пусть f: X → Y непрерывно и совместим с отношением эквивалентности через hs. Тогда Quotient.lift f hs: Quotient s → Y непрерывно.

LaTeX

$$$$ \mathrm{Continuous}(\operatorname{Quotient\_lift}(f, hs)) $$$$

Lean4

theorem quotient_lift {f : X → Y} (h : Continuous f) (hs : ∀ a b, a ≈ b → f a = f b) :
    Continuous (Quotient.lift f hs : Quotient s → Y) :=
  continuous_coinduced_dom.2 h

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