isCircuit_iff_dep_forall_diff_singleton_indep

English

If C is a circuit, then Dep C holds and for every e ∈ C, Indep(C \ {e}).

Русский

Если C — цикл, то C зависимо, и для каждого элемента e ∈ C множество C \ {e} независимо.

LaTeX

$$$M.IsCircuit(C) \iff M.Dep(C) ∧ ∀ e ∈ C, M.Indep(C \ {e})$$$

Lean4

theorem isCircuit_iff_dep_forall_diff_singleton_indep : M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ { e }) :=
  by
  wlog hCE : C ⊆ M.E
  · exact iff_of_false (hCE ∘ IsCircuit.subset_ground) (fun h ↦ hCE h.1.subset_ground)
  simp [isCircuit_iff_minimal_not_indep hCE, ← not_indep_iff hCE,
    minimal_iff_forall_diff_singleton (P := (¬M.Indep ·)) (fun _ _ hY hYX hX ↦ hY <| hX.subset hYX)]

Похожие утверждения