isCircuit_iff — Mathlib

English

Let M be a matroid and C a subset. Then C is a circuit of M if and only if C is dependent and no proper subset of C is dependent; equivalently, C is a minimal dependent subset of M.

Русский

Пусть M — матроид, и C подмножество. Тогда C является циклом M тогда и только тогда, когда C зависимо и ни одно правильное подмножество C не зависимо; то есть C минимально зависимоe подмножество M.

LaTeX

$$$M\ IsCircuit(C) \iff M.Dep(C) \wedge \forall D\ (M.Dep(D) \rightarrow D \subseteq C \rightarrow D = C)$$$

Lean4

theorem isCircuit_iff : M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D⦄, M.Dep D → D ⊆ C → D = C := by
  simp_rw [isCircuit_def, minimal_subset_iff, eq_comm (a := C)]

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