rankFinite_iff_cRank_lt_aleph0 — Mathlib

English

RankFinite is equivalent to cRank < aleph0.

Русский

Сходимость ранга равна конечной степени: RankFinite эквивалентно cRank < aleph0.

LaTeX

$$RankFinite ⇔ cRank < ℵ₀$$

Lean4

theorem rankFinite_iff_cRank_lt_aleph0 : M.RankFinite ↔ M.cRank < ℵ₀ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩
  · have ⟨B, hB, fin⟩ := h
    exact hB.cardinalMk_eq_cRank ▸ lt_aleph0_iff_finite.mpr fin
  have ⟨B, hB⟩ := M.exists_isBase
  simp_rw [← finite_coe_iff, ← lt_aleph0_iff_finite]
  exact ⟨B, hB, hB.cardinalMk_le_cRank.trans_lt h⟩

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