eventually

Mathlib.Topology.Bornology.Absorbs

URI: https://scilib.ai/kg/mathlib#Absorbs.eventually

English

If h : Absorbs M s t, then t ⊆ a • s for eventually many a in cobounded M.

Русский

Если s поглощает t, то t содержится в a·s для почти всех a из cobounded M.

LaTeX

$$$\operatorname{Absorbs} M s t \Rightarrow \forall^{\infty} a \in \operatorname{cobounded} M, \, t \subseteq a \cdot s$$$

Lean4

protected theorem eventually (h : Absorbs M s t) : ∀ᶠ a in cobounded M, t ⊆ a • s :=
  h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru