isCircuit_iff_minimal_not_indep — Mathlib

English

Let C be a subset with C ⊆ M.E. Then M.IsCircuit C holds if and only if C is a minimal not independent subset of M.

Русский

Пусть C ⊆ M.E. Тогда C является циклом M тогда и только тогда, когда C — минимальное множество, не являющееся независимым.

LaTeX

$$$C\subseteq M.E\;\Rightarrow\; M.IsCircuit(C) \iff Minimal(\lnot M.Indep\cdot)\, C$$$

Lean4

theorem isCircuit_iff_minimal_not_indep (hCE : C ⊆ M.E) : M.IsCircuit C ↔ Minimal (¬M.Indep ·) C :=
  ⟨IsCircuit.minimal_not_indep, fun h ↦
    ⟨(not_indep_iff hCE).1 h.prop, fun _ hJ hJC ↦ (h.eq_of_superset hJ.not_indep hJC).le⟩⟩

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