English
If e and f are nonloops, then closure({e}) = closure({f}) if and only if either e = f or {e, f} is not independent.
Русский
Если e и f — не петли, то closure({e}) = closure({f}) тогда и только тогда, когда либо e = f, либо {e, f} не является независимым множеством.
LaTeX
$$$M.IsNonloop e \land M.IsNonloop f \rightarrow (M.closure\(\{e\}\) = M.closure\(\{f\}\) \Leftrightarrow e = f \lor \neg M.Indep\{ e, f \})$$$
Lean4
theorem closure_eq_closure_iff_eq_or_dep (he : M.IsNonloop e) (hf : M.IsNonloop f) :
M.closure { e } = M.closure { f } ↔ e = f ∨ ¬M.Indep { e, f } :=
by
obtain (rfl | hne) := eq_or_ne e f
· exact iff_of_true rfl (Or.inl rfl)
simp_rw [he.closure_eq_closure_iff_isCircuit_of_ne hne, or_iff_right hne,
isCircuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff, singleton_subset_iff,
and_iff_left hf.mem_ground, and_iff_left he.mem_ground, and_iff_left_iff_imp]
rintro hi x (rfl | rfl)
· rwa [pair_diff_left hne, indep_singleton]
rwa [pair_diff_right hne, indep_singleton]
