cardinalInterFilter_aleph_one_iff

English

Alternative form of aleph-one equivalence with CountableInterFilter.

Русский

Другая форма эквивалентности алеф-one с CountableInterFilter.

LaTeX

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

Lean4

theorem cardinalInterFilter_aleph_one_iff : CardinalInterFilter l ℵ₁ ↔ CountableInterFilter l :=
  ⟨fun _ ↦ ⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem S ((countable_iff_lt_aleph_one S).1 h) a⟩, fun _ ↦
    CountableInterFilter.toCardinalInterFilter l⟩

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