isCompl_principal — Mathlib

English

For any subset s of α, the pair of principal filters 𝓟(s) and 𝓟(s^c) form a complemented pair in the lattice of filters.

Русский

Для любого подмножества s множества α пары 𝓟(s) и 𝓟(s^c) образуют пару дополнений в решётке фильтров.

LaTeX

$$$\\mathcal{P}(s) \\perp \\mathcal{P}(s^{c})$$$

Lean4

theorem isCompl_principal (s : Set α) : IsCompl (𝓟 s) (𝓟 sᶜ) :=
  IsCompl.of_eq (by rw [inf_principal, inter_compl_self, principal_empty]) <| by
    rw [sup_principal, union_compl_self, principal_univ]

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