hasBasis_nhds_units — Mathlib

English

The neighborhood basis at a unit γ can be taken as the singleton {γ} with the appropriate unit-indexed basis.

Русский

Базис окрестностей единицы γ может быть взят как синглтон {γ} с базисом по индексам-единицам.

LaTeX

$$$\mathcal{N}(γ) \text{ has basis } (\text{Unit})\;\{γ\}$$$

Lean4

theorem hasBasis_nhds_units (γ : Γ₀ˣ) : HasBasis (𝓝 (γ : Γ₀)) (fun _ : Unit => True) fun _ => {↑γ} :=
  hasBasis_nhds_of_ne_zero γ.ne_zero

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