countable_compl_ker — Mathlib

English

If l is countably generated and cofinite ≤ l, then the complement of the kernel of l is countable.

Русский

Если l счётно генерирован и cofinite ≤ l, то комплемент ядра l счётен.

LaTeX

$$[l.IsCountablyGenerated] → (cofinite ≤ l) → Countable(l.ker^c)$$

Lean4

/-- If `l ≥ Filter.cofinite` is a countably generated filter, then `l.ker` is cocountable. -/
theorem countable_compl_ker [l.IsCountablyGenerated] (h : cofinite ≤ l) : Set.Countable l.kerᶜ :=
  by
  rcases exists_antitone_basis l with ⟨s, hs⟩
  simp only [hs.ker, iInter_true, compl_iInter]
  exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

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