isBasis'_iff_indep_encard_eq_of_finite

English

For finite I, I is Basis' for X iff I ⊆ X, I.Indep, and I.encard = M.eRk X.

Русский

Для конечного I: I является Basis' для X тогда и только тогда, когда I ⊆ X, I независимо и I.encard = eRk X.

LaTeX

$$If $I$ is finite, then $M.IsBasis' I X$ iff $I\\subseteq X$ and $M.Indep I$ and $I.encard = M.eRk X$.$$

Lean4

theorem isBasis'_iff_indep_encard_eq_of_finite (hIfin : I.Finite) :
    M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X :=
  by
  refine ⟨fun h ↦ ⟨h.subset, h.indep, h.eRk_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩ ↦ ?_⟩
  obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIX
  rwa [hIfin.eq_of_subset_of_encard_le hIJ (hJ.encard_eq_eRk.trans hcard.symm).le]

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