quotient_map' — Mathlib

English

Continuous (Quotient.map' f H): a map on a quotient induced by a relator lifting is continuous given compatibility H.

Русский

Пусть существует непрерывность Quotient.map' f H при совместимости H.

LaTeX

$$$$ \mathrm{Continuous}(\operatorname{Quotient.map'}(f, H)) $$$$

Lean4

@[continuity, fun_prop]
theorem quotient_map' {t : Setoid Y} {f : X → Y} (hf : Continuous f) (H : (s.r ⇒ t.r) f f) :
    Continuous (Quotient.map' f H) :=
  (continuous_quotient_mk'.comp hf).quotient_lift _

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