coindep_iff_forall_subset_not_isCocircuit

English

A matroid M is coindependent on X iff every subset K ⊆ X is not a cocircuit and X ⊆ E.

Русский

Матроид M коиндепендент на X тогда и только тогда, когда каждый подмножество K ⊆ X не является кококритом и X ⊆ E.

LaTeX

$$$M.@Coindep X \iff (\forall K, K \subseteq X \rightarrow \neg M.IsCocircuit K) \land X \subseteq M.E$$$

Lean4

theorem coindep_iff_forall_subset_not_isCocircuit : M.Coindep X ↔ (∀ K, K ⊆ X → ¬M.IsCocircuit K) ∧ X ⊆ M.E :=
  indep_iff_forall_subset_not_isCircuit'

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