English
The closure in a restriction equals the intersection of the restricted closure plus the restriction, plus a part outside ground.
Русский
Замыкание в ограничении равно пересечению замыкания внутри ограниченного множества и части вне E.
LaTeX
$$$$ (M \restriction R).closure X = (M.closure (X \cap R) \cap R) \cup (R \setminus M.E). $$$$
Lean4
@[simp]
theorem restrict_closure_eq' (M : Matroid α) (X R : Set α) : (M ↾ R).closure X = (M.closure (X ∩ R) ∩ R) ∪ (R \ M.E) :=
by
obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X
obtain ⟨hI', hIR⟩ := isBasis'_restrict_iff.1 hI
ext e
rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, hI.indep.mem_closure_iff', mem_union, mem_inter_iff,
hI'.indep.mem_closure_iff', restrict_ground_eq, restrict_indep_iff, mem_diff]
by_cases he : M.Indep (insert e I)
· simp [he, and_comm, insert_subset_iff, hIR, (he.subset_ground (mem_insert ..)), imp_or]
tauto
