mem_iff_inf_principal_compl — Mathlib

English

An element s is not in a filter f iff the infimum of f with the principal of s-complement is bot.

Русский

Элемент s не принадлежит фильтру f тогда и только тогда, когда инфимум f с принципиальным фильтром по комплементу s даёт бот.

LaTeX

$$$s \\notin f \\iff f \\sqcap \\mathcal{P}(s^c) = \\bot$$$

Lean4

theorem mem_iff_inf_principal_compl {f : Filter α} {s : Set α} : s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥ :=
  by
  refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)
  exact
    ⟨fun h hs => by simpa [Set.not_nonempty_empty] using h s hs, fun hs t ht =>
      inter_compl_nonempty_iff.2 fun hts => hs <| mem_of_superset ht hts⟩

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