nonarchimedean — Mathlib

English

The neighborhood system at 0 has a basis given by the subgroups B_i.

Русский

Система окрестностей нуля имеет базис, заданный подгруппами B_i.

LaTeX

$$$(nhds 0).HasBasis (fun _ => True) fun i => B i$$

Lean4

theorem nonarchimedean (hB : SubmodulesBasis B) : @NonarchimedeanAddGroup M _ hB.topology :=
  by
  letI := hB.topology
  constructor
  intro U hU
  obtain ⟨-, ⟨i, rfl⟩, hi : (B i : Set M) ⊆ U⟩ :=
    hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU
  exact ⟨hB.openAddSubgroup i, hi⟩

Похожие утверждения