English
Let I be independent, e ∈ closure I, and e ∉ I. Then for any x, x ∈ fundCircuit e I if and only if insert e I minus {x} is independent.
Русский
Пусть I автономно; e принадлежит замыканию I и e не в I. Тогда для любого x верно: x ∈ fundCircuit e I тогда и только тогда, когда (I ∪ {e}) \\ {x} независим.
LaTeX
$$$\\forall {\\alpha} (M : Matroid \\alpha) (I : Set \\alpha) (e x : \\alpha), M.Indep I \\to e \\in M.closure I \\to e \\notin I \\to (x \\in M.fundCircuit e I \\iff M.Indep ((I \\cup \\{e\\}) \\ {x}))$$$
Lean4
theorem mem_fundCircuit_iff (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ { x }) :=
by
obtain rfl | hne := eq_or_ne x e
· simp [hI.diff, mem_fundCircuit]
suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ { x }) by
simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm, (hI.diff _).insert_indep_iff,
mem_ground_of_mem_closure hecl, heI]
refine ⟨fun h hecl ↦ (h _ diff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩
exact M.closure_subset_closure (subset_diff_singleton hJ hxJ) heJ
