absorbent_nhds_zero — Mathlib

English

Every neighborhood of the origin is absorbent.

Русский

Каждое окрестность нуля является абсорбирующим множеством.

LaTeX

$$$\\\\forall U \\\\in 𝓝(0), \\\\text{Absorbent } 𝕜 U$$$

Lean4

/-- Every neighbourhood of the origin is absorbent. -/
theorem absorbent_nhds_zero (hA : A ∈ 𝓝 (0 : E)) : Absorbent 𝕜 A :=
  absorbent_iff_inv_smul.2 fun x ↦ Filter.tendsto_inv₀_cobounded.smul tendsto_const_nhds <| by rwa [zero_smul]

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