isOpenMap_quotient_mk'_mul — Mathlib

English

The quotient map by a group action is open.

Русский

Квартирирование по группе открытое отображение мапы.

LaTeX

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

Lean4

/-- The quotient map by a group action is open, i.e. the quotient by a group action is an open
  quotient. -/
@[to_additive /-- The quotient map by a group action is open, i.e. the quotient by a group
    action is an open quotient. -/
    ]
theorem isOpenMap_quotient_mk'_mul [ContinuousConstSMul Γ T] :
    letI := MulAction.orbitRel Γ T
    IsOpenMap (Quotient.mk' : T → Quotient (MulAction.orbitRel Γ T)) :=
  fun U hU => by
  rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
  exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU

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