Documentation

Matroid.OnUniv

class Matroid.OnUniv {α : Type u_1} (M : Matroid α) :

ground_eq : M.E = Set.univ

Instances

theorem Matroid.onUniv_iff {α : Type u_1} (M : Matroid α) :

M.OnUniv ↔ M.E = Set.univ

instance Matroid.instOnUnivRestrictUniv {α : Type u_1} {M : Matroid α} :

(M.restrict Set.univ).OnUniv

instance Matroid.instOnUnivDual {α : Type u_1} {M : Matroid α} [h : M.OnUniv] :

@[simp]

theorem Matroid.ground_eq_univ {α : Type u_1} (M : Matroid α) [M.OnUniv] :

@[simp]

theorem Matroid.OnUniv.subset_ground {α : Type u_1} (M : Matroid α) [M.OnUniv] (X : Set α) :

X ⊆ M.E

theorem Matroid.OnUniv.ground_diff_eq {α : Type u_1} (M : Matroid α) [M.OnUniv] (X : Set α) :

M.E \ X = Xᶜ

theorem Matroid.corestrict_univ_eq_disjointSum {α : Type u_1} (M : Matroid α) :

(M✶.restrict Set.univ)✶ = M.disjointSum (freeOn M.Eᶜ) ⋯

@[simp]

theorem Matroid.corestrict_univ_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :

(M✶.restrict Set.univ)✶.Indep I ↔ M.Indep (I ∩ M.E)

theorem Matroid.corestrict_univ_isBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} :

(M✶.restrict Set.univ)✶.IsBase B ↔ M.IsBase (B ∩ M.E) ∧ M.Eᶜ ⊆ B

theorem Matroid.corestrict_univ_isBasis_iff {α : Type u_1} {M : Matroid α} {I X : Set α} :

(M✶.restrict Set.univ)✶.IsBasis I X ↔ M.IsBasis (I ∩ M.E) (X ∩ M.E) ∧ I ⊆ X ∧ X \ M.E ⊆ I

theorem Matroid.IsBasis'.corestrict_univ_isBasis {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) :

(M✶.restrict Set.univ)✶.IsBasis (I ∪ X \ M.E) X

theorem Matroid.IsBasis.corestrict_univ_isBasis {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) :

(M✶.restrict Set.univ)✶.IsBasis I X

theorem Matroid.IsBasis'.corestrict_univ_union_isBasis_union {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) :

(M✶.restrict Set.univ)✶.IsBasis (I ∪ M.Eᶜ) (X ∪ M.Eᶜ)

@[simp]

theorem Matroid.corestrict_univ_restrict_ground {α : Type u_1} {M : Matroid α} :

(M✶.restrict Set.univ)✶.restrict M.E = M

@[simp]

theorem Matroid.restrict_univ_restrict_ground {α : Type u_1} {M : Matroid α} :

(M.restrict Set.univ).restrict M.E = M