English
Let s be a subset of a normed division ring E acted on by 𝕜. Then s is absorbent with respect to 𝕜 if and only if for every x in E, the scalars c near 0 (with c ≠ 0) send x into s; i.e., c · x ∈ s for all c in some neighborhood of 0 excluding 0.
Русский
Пусть s — подмножество E, над которым действует 𝕜. Тогда s абсорбируется 𝕜 тогда и только тогда, когда для каждого x ∈ E скаляры c, стремящиеся к нулю и отличные от нуля, переводят x в s; то есть c · x ∈ s для всех c из некоторого окрестности нуля, исключая ноль.
LaTeX
$$$\\\\operatorname{Absorbent}_{\\\\mathbb{K}}(s) \\\\iff \\\\forall x \in E, \\\\forall^\\\\infty c \\\\in 𝓝[\\\\neq] 0, \\\\ c \\\\cdot x \\\\in s$$$
Lean4
theorem absorbent_iff_eventually_nhdsNE_zero : Absorbent 𝕜 s ↔ ∀ x : E, ∀ᶠ c : 𝕜 in 𝓝[≠] 0, c • x ∈ s :=
forall_congr' fun x ↦ by simp only [absorbs_iff_eventually_nhdsNE_zero, mapsTo_singleton]
