hasBasis_nhds_zero_adic — Mathlib

English

As above, the zero neighborhoods in I-adic topology are generated by powers of I.

Русский

Как выше, окрестности нуля в I-адической топологии задаются степенями I.

LaTeX

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

Lean4

/-- For the `I`-adic topology, the neighborhoods of zero has basis given by the powers of `I`. -/
theorem hasBasis_nhds_zero_adic (I : Ideal R) :
    HasBasis (@nhds R I.adicTopology (0 : R)) (fun _n : ℕ => True) fun n => ((I ^ n : Ideal R) : Set R) :=
  ⟨by
    intro U
    rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, h⟩
      replace h : ↑(I ^ i) ⊆ U := by simpa using h
      exact ⟨i, trivial, h⟩
    · rintro ⟨i, -, h⟩
      exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩⟩

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