English
If X is finite-rank and I is contained in X and spans X in closure, and I.encard ≤ eRk X, then I is a basis for X.
Русский
Если X конеч rank, I ⊆ X, замыкание I содержит X, и I.encard ≤ eRk X, то I — база X.
LaTeX
$$(M.IsRkFinite X) ∧ (X ⊆ M.closure I) ∧ (I ⊆ X) ∧ (I.encard ≤ M.eRk X) → M.IsBasis I X$$
Lean4
/-- If `X` is a finite-rank set, and `Y` is a superset of `X` of rank no larger than that of `X`,
then `X` and `Y` have the same closure. -/
theorem closure_eq_closure_of_subset_of_eRk_ge_eRk (hX : M.IsRkFinite X) (hXY : X ⊆ Y) (hr : M.eRk Y ≤ M.eRk X) :
M.closure X = M.closure Y := by
obtain ⟨I, hI⟩ := M.exists_isBasis' X
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)
rw [hI.eRk_eq_encard, hJ.eRk_eq_encard] at hr
rw [← closure_inter_ground, ← M.closure_inter_ground Y, ← hI.isBasis_inter_ground.closure_eq_closure, ←
hJ.isBasis_inter_ground.closure_eq_closure,
Finite.eq_of_subset_of_encard_le (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]
