The open subgroups of a nonarchimedean group are a basis of the neighbourhoods of zero

NonarchimedeanAddGroup is stated as an existence property — every neighbourhood of zero contains an open subgroup — and the filter-basis form is what consumers actually use. This module records that form once.

It is deliberately separate from TauCeti/Topology/Algebra/Nonarchimedean/FirstCountable.lean, where this statement previously lived as a have inside NonarchimedeanAddGroup.exists_antitone_basis_openAddSubgroup: that theorem additionally assumes (𝓝 0).IsCountablyGenerated, which it needs only to extract an antitone sequence from the basis. The basis itself needs no countability, so hiding it inside a first-countability result put a countability hypothesis on a statement that does not use one.

Main results

• NonarchimedeanAddGroup.nhds_zero_hasBasis_openAddSubgroup

theorem NonarchimedeanAddGroup.nhds_zero_hasBasis_openAddSubgroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] : (nhds 0).HasBasis (fun (x : OpenAddSubgroup G) => True) fun (V : OpenAddSubgroup G) => ↑V

The open additive subgroups form a basis of 𝓝 0. One direction is the defining property of NonarchimedeanAddGroup; the other is that an open subgroup is a neighbourhood of zero, since it is open and contains zero.