instTotallySeparated — Mathlib

English

A nonarchimedean group (with T2) is totally separated.

Русский

Неархимедова группа (со свойством T2) является полностью разделимой.

LaTeX

$$$\operatorname{NonarchimedeanGroup}(G) \Rightarrow \operatorname{TotallySeparatedSpace}(G)$$$

Lean4

@[to_additive]
instance (priority := 100) instTotallySeparated : TotallySeparatedSpace G where
  isTotallySeparated_univ x _ y _
    hxy := by
    obtain ⟨V, dxy⟩ := exists_openSubgroup_separating hxy
    exact
      ⟨_, _, V.isOpen.smul x, (V.isClosed.smul x).isOpen_compl, mem_own_leftCoset ..,
        dxy.subset_compl_left <| mem_own_leftCoset .., by simp, disjoint_compl_right⟩

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