hasBasis_cocardinal — Mathlib

English

The cocardinal filter has a basis given by sets of size less than c, via the complement function.

Русский

У кардинального фильтра cocardinal есть базис, задаваемый множествами размера меньше c через комплемент.

LaTeX

$$$\text{HasBasis}(cocardinal(α,hreg))\{s : Set α \mid |s| < c\} (\mathrm{compl})$$$

Lean4

theorem hasBasis_cocardinal : HasBasis (cocardinal α hreg) {s : Set α | #s < c} compl :=
  ⟨fun s =>
    ⟨fun h => ⟨sᶜ, h, (compl_compl s).subset⟩, fun ⟨_t, htf, hts⟩ =>
      by
      have : #↑sᶜ < c := by
        apply lt_of_le_of_lt _ htf
        rw [compl_subset_comm] at hts
        apply Cardinal.mk_le_mk_of_subset hts
      simp_all only [mem_cocardinal]⟩⟩

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