English
If (M / K) has a circuit C, then there exists C' with M.IsCircuit C' and C ⊆ C' ⊆ C ∪ K.
Русский
Если (M / K) имеет цикл C, то существует C' с M.IsCircuit C' и C ⊆ C' ⊆ C ∪ K.
LaTeX
$$∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K$$
Lean4
/-- If `C` is a circuit of `M ／ K`, then `M` has a circuit in the interval `[C, C ∪ K]`. -/
theorem exists_subset_isCircuit_of_contract (hC : (M ／ K).IsCircuit C) : ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K :=
by
wlog hKi : M.Indep K generalizing K with aux
· obtain ⟨I, hI⟩ := M.exists_isBasis' K
rw [hI.contract_eq_contract_delete, delete_isCircuit_iff] at hC
obtain ⟨C', hC', hCC', hC'ss⟩ := aux hC.1 hI.indep
exact ⟨C', hC', hCC', hC'ss.trans (union_subset_union_right _ hI.subset)⟩
obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_diff.1 hC.subset_ground
obtain ⟨C', hC'ss, hC'⟩ := (hKi.contract_dep_iff.1 hC.dep).2.exists_isCircuit_subset
refine ⟨C', hC', ?_, hC'ss⟩
have hdep2 : (M ／ K).Dep (C' \ K) :=
by
rw [hKi.contract_dep_iff, and_iff_right disjoint_sdiff_left]
refine hC'.dep.superset (by simp)
rw [← (hC.eq_of_dep_subset hdep2 (diff_subset_iff.2 (union_comm _ _ ▸ hC'ss)))]
exact diff_subset
