disjoint_iff_not_le — Mathlib

English

Two filters are disjoint if and only if one is not below the other.

Русский

Два фильтра попарно не совместны тогда, когда ни один не ниже другого.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} \\\\forall {g \\\\in \\\\mathrm{Filter}(\\\\alpha)}, Disjoint (\\\\uparrow f) g \\\\Leftrightarrow \\\\neg (\\\\uparrow f) \\\\le g$$$

Lean4

theorem disjoint_iff_not_le {f : Ultrafilter α} {g : Filter α} : Disjoint (↑f) g ↔ ¬↑f ≤ g := by
  rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]

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