disjoint_principal_right — Mathlib

English

Disjoint f and principal s is equivalent to s^c ∈ f.

Русский

Расхождение фильтра f и принципиального фильтра по s эквивалентно тому, что комплемент s принадлежит f.

LaTeX

$$$\\text{Disjoint}(f, \\mathcal{P}s) \\iff s^c \\in f$$$

Lean4

@[simp]
theorem disjoint_principal_right {f : Filter α} {s : Set α} : Disjoint f (𝓟 s) ↔ sᶜ ∈ f := by
  rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]

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