eventually_ne_cobounded

Mathlib.Topology.Bornology.Basic

URI: https://scilib.ai/kg/mathlib#Bornology.eventually_ne_cobounded

English

For any a in α, almost every x (with respect to cobounded filter) satisfies x ≠ a.

Русский

Для любого элемента a в α почти наверняка выполняется x ≠ a в фильтре cobounded.

LaTeX

$$$\forall a, (a \text{ fixed}) \Rightarrow ∀ᶠ x \in cobounded(α), x \neq a$$$

Lean4

theorem eventually_ne_cobounded (a : α) : ∀ᶠ x in cobounded α, x ≠ a :=
  le_cofinite_iff_eventually_ne.1 (le_cofinite _) a

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

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

Разделы

Аффилиация

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