Documentation

Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

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 #

Notation #

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)