English
If I is an independent set in M, then (M / I) has a basis B if and only if B ∪ I is a base in M and B is disjoint from I.
Русский
Пусть I независимо в M. Тогда в сокращённом по I матроиде существует базис B, если и только если B ∪ I является базисом в M и B не пересекается с I.
LaTeX
$$$ (M / I).IsBase B \;\Leftrightarrow\; M.IsBase(B \cup I) \land Disjoint(B, I) $$$
Lean4
theorem contract_isBase_iff (hI : M.Indep I) : (M ／ I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I :=
by
rw [← dual_delete_dual, dual_isBase_iff', delete_ground, dual_ground, delete_isBase_iff, subset_diff, ← and_assoc,
and_congr_left_iff, ← dual_dual M, dual_isBase_iff', dual_dual, dual_dual, union_comm, dual_ground,
union_subset_iff, and_iff_right hI.subset_ground, and_congr_left_iff, ← isBase_restrict_iff, diff_diff,
Spanning.isBase_restrict_iff, and_iff_left (diff_subset_diff_right subset_union_left)]
· simp
rwa [← dual_ground, ← coindep_iff_compl_spanning, dual_coindep_iff]
