isClosedMap_coe — Mathlib

English

If H is compact, the quotient map G → G/H is a closed map.

Русский

Если H компактна, отображение G → G/H является закрытым отображением.

LaTeX

$$$\text{IsClosedMap}((\cdot):G\to G/H) \quad \text{when } H \text{ compact}.$$$

Lean4

@[to_additive]
theorem isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) : IsClosedMap ((↑) : G → G ⧸ H) :=
  by
  intro t ht
  rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]
  exact ht.mul_right_of_isCompact hH

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