Mathlib.Data.Matroid.Dual._auxLemma.9
theorem Mathlib.Data.Matroid.Dual._auxLemma.9 :
∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.dual.Indep I = (I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B)
This theorem, from the Matroid theory in the Mathlib library, states that for any type `α`, any Matroid `M` over `α`, and any set `I` of elements of type `α`, the condition that `I` is independent in the dual of `M` is equivalent to the condition that `I` is a subset of the set of loops of `M` and that there exists a set `B` such that `B` is a base of `M` and `I` and `B` are disjoint. In the context of lattice theory, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice.
More concisely: For any matroid M over type α, a set I of elements is independent in the dual of M if and only if I is a subset of the set of loops and there exists a base B of M such that I and B are disjoint in the lattice sense.
|
Matroid.dual_base_iff
theorem Matroid.dual_base_iff :
∀ {α : Type u_1} {M : Matroid α} {B : Set α}, autoParam (B ⊆ M.E) _auto✝ → (M.dual.Base B ↔ M.Base (M.E \ B)) := by
sorry
This theorem, `Matroid.dual_base_iff`, states that for any type `α`, any matroid `M` over this type, and any set `B` of this type (with an automatic parameter ensuring that `B` is a subset of the set `E` of the matroid `M`), the set `B` is a base of the dual of the matroid `M` if and only if the complement of the set `B` with respect to `E` is a base of the matroid `M`. In mathematical terms, given a matroid `M` and a subset `B` of its ground set `E`, `B` is a base of the dual matroid if and only if the set difference `E \ B` is a base of the original matroid.
More concisely: A set is a base of the dual matroid of a matroid if and only if its complement is a base of the original matroid.
|
Matroid.dual_dual
theorem Matroid.dual_dual : ∀ {α : Type u_1} (M : Matroid α), M.dual.dual = M
This theorem, `Matroid.dual_dual`, states that for any Matroid `M` of any type `α`, the dual of the dual of `M` is equal to `M` itself. In other words, applying the dual operation twice on a matroid returns the original matroid. This theorem mirrors the common mathematical principle that the double dual (or double transpose) of many mathematical objects is the object itself.
More concisely: The dual of a matroid is equal to its own dual.
|