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 in G.

References

See Proposition 2.3.9 and Problem 63 in F. Q. Gouvêa, p-adic numbers.

theorem NonarchimedeanAddGroup.exists_openAddSubgroup_separating {G : Type u_1} [TopologicalSpace G] [AddGroup G] [NonarchimedeanAddGroup G] [T2Space G] {a : G} {b : G} (h : a ≠ b) : ∃ (V : OpenAddSubgroup G), Disjoint (a +ᵥ ↑V) (b +ᵥ ↑V)

theorem NonarchimedeanGroup.exists_openSubgroup_separating {G : Type u_1} [TopologicalSpace G] [Group G] [NonarchimedeanGroup G] [T2Space G] {a : G} {b : G} (h : a ≠ b) : ∃ (V : OpenSubgroup G), Disjoint (a • ↑V) (b • ↑V)

@[instance 100]

instance NonarchimedeanAddGroup.instTotallySeparated {G : Type u_1} [TopologicalSpace G] [AddGroup G] [NonarchimedeanAddGroup G] [T2Space G] : TotallySeparatedSpace G

Equations

• ⋯ = ⋯

@[instance 100]

instance NonarchimedeanGroup.instTotallySeparated {G : Type u_1} [TopologicalSpace G] [Group G] [NonarchimedeanGroup G] [T2Space G] : TotallySeparatedSpace G

Equations

• ⋯ = ⋯