hasBasis_nhds_adic — Mathlib

English

HasBasis for nhds at x in the adic topology given by translates x + I^n.

Русский

HasBasis для окрестностей в x в адической топологии задаётся переносами x + I^n.

LaTeX

$$$HasBasis\\;(@nhds\\;R\\;I.adicTopology\\;x)\\;...$$$

Lean4

theorem hasBasis_nhds_adic (I : Ideal R) (x : R) :
    HasBasis (@nhds R I.adicTopology x) (fun _n : ℕ => True) fun n => (fun y => x + y) '' (I ^ n : Ideal R) :=
  by
  letI := I.adicTopology
  have := I.hasBasis_nhds_zero_adic.map fun y => x + y
  rwa [map_add_left_nhds_zero x] at this

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