English
If I is independent, e lies in the closure of I, and e is not in I, then the fundamental circuit of e relative to I is a circuit.
Русский
Если I независимо, e принадлежит замыканию I, и e не принадлежит I, тогда фундаментальная окружность e относительно I является окружностью.
LaTeX
$$$\\forall \\alpha\\ (M : Matroid \\alpha)\\ (I : Set \\alpha)\\ (e : \\alpha), M.Indep I \\to e \\in M.closure I \\to e \\notin I \\to M.IsCircuit (M.fundCircuit e I)$$$
Lean4
theorem fundCircuit_isCircuit (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
M.IsCircuit (M.fundCircuit e I) :=
by
have aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I := sInter_subset_of_mem (by simpa)
rw [fundCircuit_eq_sInter hecl]
refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_
· simp [show ∃ x ⊆ I, e ∈ M.closure x ∧ e ∉ x from ⟨I, by simp [hecl, heI]⟩]
· rw [hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)]
simp
simp only [mem_sInter, mem_setOf_eq, and_imp]
exact fun f hf hecl ↦ (hf _ (diff_subset.trans aux) hecl).2 rfl
