eventually_nhds_zero — Mathlib

English

If Absorbs 𝕜 s t and 0 ∈ s, then c • · sends t into s for all c sufficiently near 0.

Русский

Если s абсорбируется t относительно 𝕜 и 0 ∈ s, то для скаляра c, близкого к нулю, отображение x ↦ c · x отправляет t в s для всех достаточно маленьких c.

LaTeX

$$$\\forall \\text{(h : Absorbs } \\mathbb{K}\\ s\\ t)\\, (h_0 : 0 \\in s), \\forall^\\infty c \\in 𝓝 0, \\ operatorname{MapsTo} (c \\cdot \\cdot) \\ t \\ s$$$

Lean4

theorem eventually_nhds_zero (h : Absorbs 𝕜 s t) (h₀ : 0 ∈ s) : ∀ᶠ c : 𝕜 in 𝓝 0, MapsTo (c • ·) t s :=
  (absorbs_iff_eventually_nhds_zero h₀).1 h

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