quotient_liftOn' — Mathlib

English

If f: X → Y is continuous and hs respects equivalence classes, then Quotient.liftOn' x f hs is continuous on Quotient s → Y.

Русский

Пусть f: X → Y непрерывно и hs согласован с эквивалентностями; тогда Quotient.liftOn' x f hs непрерывно на Quotient s → Y.

LaTeX

$$$$ \mathrm{Continuous}(\operatorname{Quotient.liftOn'}(x, f, hs)) $$$$

Lean4

theorem quotient_liftOn' {f : X → Y} (h : Continuous f) (hs : ∀ a b, s a b → f a = f b) :
    Continuous (fun x => Quotient.liftOn' x f hs : Quotient s → Y) :=
  h.quotient_lift hs

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