dense_preimage_mk — Mathlib

English

Let G be a topological group and N a subgroup. Let π: G → G/N be the natural quotient map. For any subset s of the quotient G/N, the preimage π^{-1}(s) is dense in G if and only if s is dense in G/N.

Русский

Пусть G — топологическая группа, N — подгруппа. Пусть π: G → G/N — естественное отображение-околоткование. Для любого подмножества s ⊆ G/N выполнено, что предобраз π^{-1}(s) плотно в G тогда и только тогда, когда s плотно в G/N.

LaTeX

$$$\operatorname{Dense}(\pi^{-1}(s)) \iff \operatorname{Dense}(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem dense_preimage_mk {s : Set (G ⧸ N)} : Dense ((↑) ⁻¹' s : Set G) ↔ Dense s :=
  isOpenQuotientMap_mk.dense_preimage_iff

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