cRank_le_iff — Mathlib

English

Characterization: cRk X ≤ κ if and only if every basis I of X satisfies |I| ≤ κ.

Русский

Характеризация: cRk(X) ≤ κ тогда и только тогда, когда для каждой базы I X выполняется |I| ≤ κ.

LaTeX

$$$M.cRk X \\le \\kappa \\iff \\forall I, M.IsBasis' I X \\rightarrow |I| \\le \\kappa$$$

Lean4

theorem cRank_le_iff : M.cRank ≤ κ ↔ ∀ ⦃B⦄, M.IsBase B → #B ≤ κ :=
  ⟨fun h _ hB ↦ (hB.cardinalMk_le_cRank.trans h), fun h ↦ ciSup_le fun ⟨_, hB⟩ ↦ h hB⟩

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