le_sup_iff — Mathlib

English

For an ultrafilter u and filters f,g, u ≤ f ⊔ g iff u ≤ f or u ≤ g.

Русский

Для ульрафильтра u и фильтров f,g верно: u ≤ f ⊔ g iff u ≤ f или u ≤ g.

LaTeX

$$$\\\\forall {u \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {f,g \\\\in \\\\mathrm{Filter}(\\\\alpha)}, \\\\; u \\\\le f \\\\sqcup g \\\\Leftrightarrow (u \\\\le f) \\\\lor (u \\\\le g)$$$

Lean4

@[simp]
theorem le_sup_iff {u : Ultrafilter α} {f g : Filter α} : ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g :=
  not_iff_not.1 <| by simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

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