le_cofinite_iff_eventually_ne

Mathlib.Order.Filter.Cofinite

URI: https://scilib.ai/kg/mathlib#Filter.le_cofinite_iff_eventually_ne

English

A filter l is below cofinite iff for every x, eventually in l, y ≠ x.

Русский

Фильтр l меньше cofinite тогда и только тогда, для каждого x верно: часто y ≠ x в l.

LaTeX

$$$l \le \operatorname{cofinite} \iff \forall x, \forall^\infty y \in l, y \neq x$$$

Lean4

theorem le_cofinite_iff_eventually_ne : l ≤ cofinite ↔ ∀ x, ∀ᶠ y in l, y ≠ x :=
  le_cofinite_iff_compl_singleton_mem

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

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

Разделы

Аффилиация

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