hasBasis_nhds_zero — Mathlib

English

The neighborhood filter of 0 has a basis consisting of the sets Iio(γ) for γ ≠ 0.

Русский

Фильтр окрестностей нуля имеет базис из множеств Iio(γ) при γ ≠ 0.

LaTeX

$$$\mathcal{N}(0)\text{ has basis } {Iio(\gamma) : \gamma \ne 0}$$$

Lean4

/-- In a linearly ordered group with zero element adjoined, `U` is a neighbourhood of `0` if and
only if there exists a nonzero element `γ₀` such that `Iio γ₀ ⊆ U`. -/
theorem hasBasis_nhds_zero : (𝓝 (0 : Γ₀)).HasBasis (fun γ : Γ₀ => γ ≠ 0) Iio :=
  by
  rw [nhds_zero]
  refine hasBasis_biInf_principal ?_ ⟨1, one_ne_zero⟩
  exact directedOn_iff_directed.2 (Monotone.directed_ge fun a b hab => Iio_subset_Iio hab)

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