setOf_dep_eq — Mathlib

English

The set of dependent subsets equals the not-independent subsets contained in the ground set.

Русский

Множество зависимых подмножеств совпадает с множеством подмножеств, не являющихся независимыми и содержащихся в грунтовом множестве.

LaTeX

$$$ \{ D \mid M.Dep D \} = (\{ I \mid \neg M.Indep I \}) \cap \{ I \mid I \subseteq M.E \}$$$

Lean4

theorem setOf_dep_eq (M : Matroid α) : {D | M.Dep D} = {I | M.Indep I}ᶜ ∩ Iic M.E :=
  rfl

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