minimal_not_indep — Mathlib

English

For a circuit C of M, C is a minimal not independent set; i.e., any proper subset of C is independent.

Русский

Для цикла C матроида M C является минимальным множеством, не являющимся независимым; то есть любое подмножество C является независимым.

LaTeX

$$$\text{Minimal}(\lnot M.Indep\cdot)\, C$ for a circuit C; equivalently, if M.IsCircuit(C) then for all proper subsets D of C, M.Indep(D).$$

Lean4

theorem minimal_not_indep (hC : M.IsCircuit C) : Minimal (¬M.Indep ·) C :=
  by
  simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]
  exact fun ⦃t⦄ a ↦ ssubset_indep hC a

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