cofinite_inf_principal_compl — Mathlib

English

If s is finite, then the infimum of the cofinite filter and the principal filter on s^c is equal to the cofinite filter: cofinite ⊓ 𝓟(s^c) = cofinite.

Русский

Если s конечна, то инфимум кофинитного фильтра и принципиального фильтра на дополнение к s равен кофинитному фильтру: cofinite ⊓ 𝓟(s^c) = cofinite.

LaTeX

$$$\\operatorname{cofinite} \\wedge \\mathcal{P}(s^{c}) = \\operatorname{cofinite}$$$

Lean4

theorem cofinite_inf_principal_compl {s : Set α} (hs : s.Finite) : cofinite ⊓ 𝓟 sᶜ = cofinite := by
  simpa using hs.compl_mem_cofinite

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