toCountableInterFilter — Mathlib

English

If l is a CardinalInterFilter with c > ℵ₀, then l is CountableInterFilter.

Русский

Если l — CardinalInterFilter с кардиналом c > ℵ₀, то l является CountableInterFilter.

LaTeX

$$$$ (\\text{CardinalInterFilter } l c) \\land (ℵ_0 < c) \\Rightarrow CountableInterFilter\ l $$$$

Lean4

/-- Every CardinalInterFilter with c > ℵ₀ is a CountableInterFilter -/
theorem toCountableInterFilter (l : Filter α) [CardinalInterFilter l c] (hc : ℵ₀ < c) : CountableInterFilter l where
  countable_sInter_mem S hS
    a := CardinalInterFilter.cardinal_sInter_mem S (lt_of_le_of_lt (Set.Countable.le_aleph0 hS) hc) a

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