isOpenQuotientMap_quotientMk — Mathlib

English

The quotient map (Quotient.mk') is an open quotient map.

Русский

Квотирующая карта mk' является открытым квотоидным отображением.

LaTeX

$$$IsOpenQuotientMap (Quotient.mk' : T \to Quotient (MulAction.orbitRel \Gamma T))$$$

Lean4

@[to_additive]
theorem isOpenQuotientMap_quotientMk [ContinuousConstSMul Γ T] :
    IsOpenQuotientMap (Quotient.mk (MulAction.orbitRel Γ T)) :=
  ⟨Quot.mk_surjective, continuous_quot_mk, isOpenMap_quotient_mk'_mul⟩

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