absorbs_iff_eventually_nhdsNE_zero

English

Absorbs 𝕜 s t is equivalent to the property that for scalars c near 0 (excluding 0) the map x ↦ c•x sends t into s eventually.

Русский

Absorbs 𝕜 s t эквивалентно тому, что для скаляров c, приближающихся к 0 (кроме 0), отображение x ↦ c•x переводит t в s вплоть до предела.

LaTeX

$$$\text{Absorbs}_{𝕜}(s,t) \iff \forall^{\!} c : 𝕜 \text{ in } 𝓝[≠] 0,\; \mathrm{MapsTo}(c\cdot -)\, t\, s$$$

Lean4

theorem absorbs_iff_eventually_nhdsNE_zero : Absorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝[≠] 0, MapsTo (c • ·) t s := by
  rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]; rfl

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