English
For C contained in the ground set, M.IsCircuit C iff Dep C and every I ⊂ C is independent.
Русский
Для C, заключенного в базовую площадку, C является циклe M тогда и только тогда, когда Dep C и каждое подмножество I ⊂ C независимо.
LaTeX
$$$C \subseteq M.E \Rightarrow M.IsCircuit(C) \iff M.Dep(C) ∧ ∀ I, I ⊂ C \Rightarrow M.Indep(I)$$$
Lean4
theorem insert_isCircuit_of_forall (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.closure I)
(h : ∀ f ∈ I, e ∉ M.closure (I \ { f })) : M.IsCircuit (insert e I) :=
by
rw [isCircuit_iff_dep_forall_diff_singleton_indep, hI.insert_dep_iff, and_iff_right ⟨he, heI⟩]
rintro f (rfl | hfI)
· simpa [heI]
rw [← insert_diff_singleton_comm (by rintro rfl; contradiction),
(hI.diff _).insert_indep_iff_of_notMem (by simp [heI])]
exact ⟨mem_ground_of_mem_closure he, h f hfI⟩
