English
If X is finite-rank and X ⊆ Y and eRk Y ≤ eRk X, then closure X = closure Y.
Русский
Если X имеет конечный ранг, X ⊆ Y и eRk Y ≤ eRk X, то замыкания X и Y совпадают.
LaTeX
$$(M.IsRkFinite X) ∧ (X ⊆ Y) ∧ (M.eRk Y ≤ M.eRk X) → M.closure X = M.closure Y$$
Lean4
/-- If `X` is a finite-rank set, and `I` is a subset of `X` of cardinality
no larger than the rank of `X` that spans `X`, then `I` is a basis for `X`. -/
theorem isBasis_of_subset_closure_of_subset_of_encard_le (hX : M.IsRkFinite X) (hXI : X ⊆ M.closure I) (hIX : I ⊆ X)
(hI : I.encard ≤ M.eRk X) : M.IsBasis I X :=
by
obtain ⟨J, hJ⟩ := M.exists_isBasis (I ∩ M.E)
have hIJ := hJ.subset.trans inter_subset_left
rw [← closure_inter_ground] at hXI
replace hXI := hXI.trans <| M.closure_subset_closure_of_subset_closure hJ.subset_closure
have hJX := hJ.indep.isBasis_of_subset_of_subset_closure (hIJ.trans hIX) hXI
rw [← hJX.encard_eq_eRk] at hI
rwa [← Finite.eq_of_subset_of_encard_le (hX.finite_of_isBasis hJX) hIJ hI]
