isBasis'_of_eRk_ge — Mathlib

English

Equivalent restatement of the finite Criterion for Basis' with the same conditions.

Русский

Эквивалентная формулировка конечного критерия Basis'.

LaTeX

$$Equivalent restatement of the finite Basis' criterion: $I$ finite and $M.IsBasis' I X$ iff $I\\subseteq X$, $M.Indep I$, and $I.encard = M.eRk X$.$$

Lean4

/-- If `I` is a finite independent subset of `X` for which `M.eRk X ≤ M.eRk I`,
then `I` is a `Basis'` for `X`. -/
theorem isBasis'_of_eRk_ge (hI : M.Indep I) (hIfin : I.Finite) (hIX : I ⊆ X) (h : M.eRk X ≤ M.eRk I) : M.IsBasis' I X :=
  (isBasis'_iff_indep_encard_eq_of_finite hIfin).2 ⟨hIX, hI, by rw [h.antisymm (M.eRk_mono hIX), hI.eRk_eq_encard]⟩

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