compl_notMem_iff — Mathlib

English

For any ultrafilter f and set s, s^c ∉ f iff s ∈ f.

Русский

Для любого ульрафильтра f и множества s верно: s^c ∉ f ⇔ s ∈ f.

LaTeX

$$$\\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {s \\\\subseteq \\\\alpha}, s^c \notin f \\\\Leftrightarrow s \\in f$$$

Lean4

@[simp]
theorem compl_notMem_iff : sᶜ ∉ f ↔ s ∈ f :=
  ⟨fun hsc => le_principal_iff.1 <| f.le_of_inf_neBot ⟨fun h => hsc <| mem_of_eq_bot <| by rwa [compl_compl]⟩,
    compl_notMem⟩

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