English
If h is a basis I X in M and hJC is a special basis J C, and I \\ C ∪ J is independent, then the contracted matroid M / C has I \\ C as a basis for X \\ C.
Русский
Пусть h: MIsBasis I X и hJC: MIsBasis' J C, и I \\ C ∪ J независимы в M. Тогда после сокращения по C матроид M / C имеет I \\ C как базис для X \\ C.
LaTeX
$$$(M / C).IsBasis(I \\ C) (X \\ C)$$$
Lean4
theorem contract_isBasis_of_isBasis' (h : M.IsBasis I X) (hJC : M.IsBasis' J C) (h_ind : M.Indep (I \ C ∪ J)) :
(M ／ C).IsBasis (I \ C) (X \ C) := by
have hIX := h.subset
have hJCss := hJC.subset
rw [hJC.contract_eq_contract_delete, delete_isBasis_iff]
refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
rotate_left
· rw [closure_union_congr_right hJC.closure_eq_closure, diff_union_self,
closure_union_congr_left h.closure_eq_closure]
exact
subset_closure_of_subset' _ (by tauto_set)
(union_subset (diff_subset.trans h.subset_ground) hJC.indep.subset_ground)
all_goals tauto_set
