disjoint_cofinite_right

Mathlib.Order.Filter.Cofinite

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

English

Disjoint l cofinite is equivalent to the existence of a finite s in l.

Русский

Беспересечение l и кофинитного фильтра эквивалентно существованию конечного s в l.

LaTeX

$$Disjoint l cofinite ⇔ ∃ s ∈ l, Finite s$$

Lean4

theorem disjoint_cofinite_right : Disjoint l cofinite ↔ ∃ s ∈ l, Set.Finite s :=
  disjoint_comm.trans disjoint_cofinite_left

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

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

Разделы

Аффилиация

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