cRank_eq_iSup_cardinalMk_indep — Mathlib

English

If I is independent and I ⊆ X, then |I| ≤ M.cRk X.

Русский

Если I независимо и I ⊆ X, то |I| ≤ cRk(X).

LaTeX

$$$|I| \\le M.cRk(X)$$$

Lean4

theorem cRank_eq_iSup_cardinalMk_indep : M.cRank = ⨆ I : { I // M.Indep I }, #I :=
  (ciSup_le' fun B ↦ le_ciSup_of_le (bddAbove_range _) ⟨B, B.2.indep⟩ <| by rfl).antisymm <|
    ciSup_le' fun I ↦
      have ⟨B, isBase, hIB⟩ := I.2.exists_isBase_superset
      le_ciSup_of_le (bddAbove_range _) ⟨B, isBase⟩ (mk_le_mk_of_subset hIB)

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