English
A version of the spanning criterion without the supportedness hypothesis: (M / C).Spanning X holds exactly when M.Spanning (X ∪ (C ∩ M.E)) holds and X is disjoint from C.
Русский
Версия критерия охвата без предположения о поддержке: (M / C).Spanning X эквивалентно M.Spanning (X ∪ (C ∩ M.E)) и X ∩ C = ∅.
LaTeX
$$(M ／ C).Spanning X ↔ M.Spanning (X ∪ (C ∩ M.E)) ∧ Disjoint X C$$
Lean4
/-- A version of `Matroid.contract_spanning_iff` without the supportedness hypothesis. -/
theorem contract_spanning_iff' : (M ／ C).Spanning X ↔ M.Spanning (X ∪ (C ∩ M.E)) ∧ Disjoint X C :=
by
rw [← contract_inter_ground_eq, contract_spanning_iff, and_congr_right_iff]
refine fun h ↦ ⟨fun hdj ↦ ?_, Disjoint.mono_right inter_subset_left⟩
rw [← diff_union_inter C M.E, disjoint_union_right, and_iff_left hdj]
exact disjoint_sdiff_right.mono_left (subset_union_left.trans h.subset_ground)
