of_boundedSpace

Mathlib.Topology.Bornology.Absorbs

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

English

Same as above for another instance; absorbing relation yields eventual containment.

Русский

То же самое для другой инстанции; отношение поглощения даёт конечное включение.

LaTeX

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

Lean4

@[simp]
theorem of_boundedSpace [BoundedSpace M] : Absorbs M s t := by simp [Absorbs]

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

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

Разделы

Аффилиация

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