hasBasis_nhds — Mathlib

English

For every a ∈ A, the neighborhoods of a form a basis given by translates a + B_i.

Русский

Для каждого a ∈ A окрестности a образуют базис, заданный переходами a + B_i.

LaTeX

$$$(nhds x).HasBasis (\\lambda _ \\to True) \\to (x + ·) '' ↑(B i)$$$

Lean4

theorem hasBasis_nhds (a : A) : HasBasis (@nhds A hB.topology a) (fun _ => True) fun i => {b | b - a ∈ B i} :=
  ⟨by
    intro s
    rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
    simp only [true_and]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, hi⟩
      use i
      suffices h : {b : A | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
        by
        rw [h]
        assumption
      simp only [image_add_left, neg_add_eq_sub]
      ext b
      simp
    · rintro ⟨i, hi⟩
      use B i
      constructor
      · use i
      · rw [image_subset_iff]
        rintro b b_in
        apply hi
        simpa using b_in⟩

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