English
Two distinct nonloops e and f satisfy that their closures are equal if and only if {e, f} is a circuit.
Русский
Две различные не петли e и f имеют равные замыкания тогда и только тогда, когда {e, f} образует цикл.
LaTeX
$$$M.IsNonloop e \land e \neq f \rightarrow (M.closure\(\{e\}\) = M.closure\(\{f\}\) \Leftrightarrow M.IsCircuit\(\{e, f\}\))$$$
Lean4
/-- Two distinct nonloops with the same closure form a circuit. -/
theorem closure_eq_closure_iff_isCircuit_of_ne (he : M.IsNonloop e) (hef : e ≠ f) :
M.closure { e } = M.closure { f } ↔ M.IsCircuit { e, f } :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· have hf := he.isNonloop_of_mem_closure (by rw [← h]; exact M.mem_closure_self e)
rw [isCircuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff, and_iff_right he.mem_ground,
singleton_subset_iff, and_iff_left hf.mem_ground]
suffices ¬M.Indep { e, f } by simpa [pair_diff_left hef, hf, pair_diff_right hef, he]
rw [Indep.insert_indep_iff_of_notMem (by simpa) (by simpa)]
simp [← h, mem_closure_self _ _ he.mem_ground]
have hclosure := (h.closure_diff_singleton_eq e).trans (h.closure_diff_singleton_eq f).symm
rwa [pair_diff_left hef, pair_diff_right hef, eq_comm] at hclosure
