isCircuit_iff_forall_ssubset — Mathlib

English

A circuit C is equivalent to being dependent and every subset I ⊂ C is independent.

Русский

Цикл C эквивалентен тому, что C зависит, и любое подмножество I ⊂ C независимо.

LaTeX

$$$M.IsCircuit(C) \iff M.Dep(C) \land \forall \{I\}, I\subset C \Rightarrow M.Indep(I)$$$

Lean4

theorem isCircuit_iff_forall_ssubset : M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I⦄, I ⊂ C → M.Indep I :=
  by
  rw [IsCircuit, minimal_iff_forall_ssubset, and_congr_right_iff]
  exact fun h ↦
    ⟨fun h' I hIC ↦ ((not_dep_iff (hIC.subset.trans h.subset_ground)).1 (h' hIC)), fun h I hIC ↦ (h hIC).not_dep⟩

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