English
If C is a circuit contained in insert e I, and I is independent, then C equals the fundamental circuit e relative to I.
Русский
Если C является окружностью, содержащейся внутри вставки e в I, и I независим, тогда C равно фундаментальному фундконтуру e относительно I.
LaTeX
$$$\\forall {\\alpha} (M : Matroid \\alpha) {C I : Set \\alpha} {e : \\alpha}, M.IsCircuit C \\to M.Indep I \\to C \\subseteq \\mathrm{insert}(e,I) \\to C = M.fundCircuit e I$$$
Lean4
/-- For `I` independent, `M.fundCircuit e I` is the only circuit contained in `insert e I`. -/
theorem eq_fundCircuit_of_subset (hC : M.IsCircuit C) (hI : M.Indep I) (hCs : C ⊆ insert e I) : C = M.fundCircuit e I :=
by
obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCs
· exact (hC.not_indep (hI.subset hCI)).elim
suffices hss : M.fundCircuit e I ⊆ C
by
refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss
· rw [hI.mem_closure_iff]
exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))
exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))
have heCcl := (hC.diff_singleton_isBasis heC).subset_closure heC
have heI : e ∈ M.closure I := M.closure_subset_closure hCeI heCcl
rw [fundCircuit_eq_sInter heI]
refine insert_subset heC <| (sInter_subset_of_mem (t := C \ { e }) ?_).trans diff_subset
exact ⟨hCeI, heCcl⟩
