English
Assume 0 ∈ s. Then s absorbs t with respect to 𝕜 if and only if for every near-zero scalar c, the map x ↦ c · x sends t into s; i.e., MapsTo (c · ·) t s holds eventually near 0.
Русский
Пусть 0 принадлежит s. Тогда s абсорбирует t относительно 𝕜 тогда и только тогда, когда при любом скалярном множителе c близком к нулю отображение x ↦ c · x переводит множество t в s; то есть для всех близких к нулю c верно, что MapsTo (c · ·) t s.
LaTeX
$$$\\bigl( Absorbs \\mathbb{K}\\ s\\ t \\bigr) \\iff \\forall^\\infty c \\in 𝓝 0, \\ operatorname{MapsTo} (c \\cdot \\cdot)\, t\, s$$$
Lean4
theorem absorbs_iff_eventually_nhds_zero (h₀ : 0 ∈ s) : Absorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝 0, MapsTo (c • ·) t s :=
by
rw [← nhdsNE_sup_pure, Filter.eventually_sup, Filter.eventually_pure, ← absorbs_iff_eventually_nhdsNE_zero,
and_iff_left]
intro x _
simpa only [zero_smul]
