Total separatedness of nonarchimedean groups #
In this file, we prove that a nonarchimedean group is a totally separated topological space. The fact that a nonarchimedean group is a totally disconnected topological space is implied by the fact that a nonarchimedean group is totally separated.
Main results #
NonarchimedeanGroup.instTotallySeparated: A nonarchimedean group is a totally separated topological space.
Notation #
G: Is a nonarchimedean group.V: Is an open subgroup which is a neighbourhood of the identity inG.
References #
See Proposition 2.3.9 and Problem 63 in F. Q. Gouvêa, p-adic numbers.
theorem NonarchimedeanGroup.exists_openSubgroup_separating {G : Type u_1} [TopologicalSpace G] [Group G] [NonarchimedeanGroup G] [T2Space G] {a b : G} (h : a ≠ b) :
∃ (V : OpenSubgroup G), Disjoint (a • ↑V) (b • ↑V)
theorem NonarchimedeanAddGroup.exists_openAddSubgroup_separating {G : Type u_1} [TopologicalSpace G] [AddGroup G] [NonarchimedeanAddGroup G] [T2Space G] {a b : G} (h : a ≠ b) :
∃ (V : OpenAddSubgroup G), Disjoint (a +ᵥ ↑V) (b +ᵥ ↑V)
@[instance 100]
instance NonarchimedeanGroup.instTotallySeparated {G : Type u_1} [TopologicalSpace G] [Group G] [NonarchimedeanGroup G] [T2Space G] :
@[instance 100]
instance NonarchimedeanAddGroup.instTotallySeparated {G : Type u_1} [TopologicalSpace G] [AddGroup G] [NonarchimedeanAddGroup G] [T2Space G] :