dense_image_mk — Mathlib

English

Let G be a topological group and N a subgroup with quotient map q: G → G/N. For any subset s of G, the image mk''s in the quotient is dense in G/N if and only if the product sN is dense in G, where sN = {sn : s ∈ s, n ∈ N}.

Русский

Пусть G — топологическая группа, N — подгруппа, q: G → G/N — проекция. Для любого подмножества s ⊆ G плотность образа q''s в G/N эквивалентна плотности множества sN в G, где sN = {sn : s ∈ s, n ∈ N}.

LaTeX

$$$\operatorname{Dense}(\mathrm{mk}''s) \iff \operatorname{Dense}(s \cdot N)$$$

Lean4

@[to_additive]
theorem dense_image_mk {s : Set G} : Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by
  rw [← dense_preimage_mk, preimage_image_mk_eq_mul]

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