hasBasis_nhds_zero — Mathlib

English

The neighborhoods of zero in a RingSubgroupsBasis are generated by the subgroups B_i.

Русский

Окрестности нуля в RingSubgroupsBasis образуют базис из подгрупп B_i.

LaTeX

$$$(nhds 0).HasBasis (\\lambda _ \\to True) \\rightarrow \\) fun i => B i$$

Lean4

theorem hasBasis_nhds_zero : HasBasis (@nhds A hB.topology 0) (fun _ => True) fun i => B i :=
  ⟨by
    intro s
    rw [hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, hi⟩
      exact ⟨i, trivial, hi⟩
    · rintro ⟨i, -, hi⟩
      exact ⟨B i, ⟨i, rfl⟩, hi⟩⟩

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