hasBasis_nhds — Mathlib

English

For any x in R, the neighborhoods of x have a basis given by translates x + I^n.

Русский

Для любого элемента x в R окрестности x имеют базис, состоящий из смещений x + I^n.

LaTeX

$$$(nhds x).HasBasis (\\lambda _ \\to True) (\\lambda n \\to (x + \\cdot) '' ↑(I^n))$$$

Lean4

theorem hasBasis_nhds {I : Ideal R} (hI : IsAdic I) (x : R) :
    (𝓝 x).HasBasis (fun _ ↦ True) fun n ↦ (x + ·) '' ↑(I ^ n) :=
  hI ▸ Ideal.hasBasis_nhds_adic I x

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