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]
: