toCardinalInterFilter — Mathlib

English

CardinalInterFilter l ℵ₁ is equivalent to CountableInterFilter l.

Русский

CardinalInterFilter l ℵ₁ эквивалентен CountableInterFilter l.

LaTeX

$$$$ CardinalInterFilter\\ l\\ \\aleph_1 \\iff CountableInterFilter\\ l $$$$

Lean4

/-- Every CountableInterFilter is a CardinalInterFilter with c = ℵ₁ -/
instance toCardinalInterFilter (l : Filter α) [CountableInterFilter l] : CardinalInterFilter l ℵ₁ where
  cardinal_sInter_mem S hS a := CountableInterFilter.countable_sInter_mem S ((countable_iff_lt_aleph_one S).mpr hS) a

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