isRkFinite_iff_cRk_lt_aleph0 — Mathlib

English

Let M be a matroid on α and X ⊆ α. The rank of X is finite if and only if the cRk (cardinal rank) of X is less than aleph-null: rk_M(X) < ∞ if and only if cRk_M(X) < aleph_0.

Русский

Пусть M — матроид над α и X ⊆ α. Ранг множества X конечен тогда и только тогда, когда кардинальный ранг cRk_M(X) меньше aleph_0: rk_M(X) < ∞ тогда и только тогда, когда cRk_M(X) < aleph_0.

LaTeX

$$$\\operatorname{rk}_M(X) < \\infty \\iff M.cRk(X) < \\aleph_0$$$

Lean4

theorem isRkFinite_iff_cRk_lt_aleph0 : M.IsRkFinite X ↔ M.cRk X < ℵ₀ := by
  rw [IsRkFinite, rankFinite_iff_cRank_lt_aleph0, cRank_restrict]

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