disjoint_cofinite_left

Mathlib.Order.Filter.Cofinite

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

English

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

Русский

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

LaTeX

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

Lean4

theorem disjoint_cofinite_left : Disjoint cofinite l ↔ ∃ s ∈ l, Set.Finite s := by
  simp [l.basis_sets.disjoint_iff_right]

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

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

Разделы

Аффилиация

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