le_eRk_iff — Mathlib

English

For any X and n, n ≤ eRk(X) iff there exists I ⊆ X with I indep and I.encard = n.

Русский

Для любых X и n выполняется: n ≤ eRk(X) тогда и только тогда существует I ⊆ X с I независимо и I.encard = n.

LaTeX

$$$ n \\le M.eRk(X) \\iff \\exists I, I \\subseteq X \\land M.Indep I \\land I.encard = n $$$

Lean4

theorem le_eRk_iff : n ≤ M.eRk X ↔ ∃ I, I ⊆ X ∧ M.Indep I ∧ I.encard = n :=
  by
  refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩
  · obtain ⟨J, hJ⟩ := M.exists_isBasis' X
    rw [← hJ.encard_eq_eRk] at h
    obtain ⟨I, hIJ, rfl⟩ := exists_subset_encard_eq h
    exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩
  rw [← hIc, ← hI.eRk_eq_encard]
  exact M.eRk_mono hIX

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