def Matroid.project {α : Type u_1} (M : Matroid α) (C : Set α) : Matroid α

Contract a set C, then put the removed elements back in as loops.

Equations

• M.project C = (M.contract C).restrict M.E

@[simp]

theorem Matroid.project_ground {α : Type u_1} (M : Matroid α) (C : Set α) : (M.project C).E = M.E

@[simp]

theorem Matroid.project_inter_ground {α : Type u_1} (M : Matroid α) (C : Set α) : M.project (C ∩ M.E) = M.project C

@[simp]

theorem Matroid.project_closure {α : Type u_1} (M : Matroid α) (C X : Set α) : (M.project C).closure X = M.closure (X ∪ C)

theorem Matroid.project_closure_eq_project_closure_union {α : Type u_1} (M : Matroid α) (C X : Set α) : (M.project C).closure X = (M.project C).closure (X ∪ C)

theorem Matroid.project_closure_congr {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.closure X = M.closure Y) (C : Set α) : (M.project C).closure X = (M.project C).closure Y

theorem Matroid.project_indep_iff {α : Type u_1} {M : Matroid α} {I C : Set α} : (M.project C).Indep I ↔ (M.contract C).Indep I

theorem Matroid.project_indep_eq {α : Type u_1} {M : Matroid α} {C : Set α} : (M.project C).Indep = (M.contract C).Indep

theorem Matroid.Indep.project_indep_iff {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) : (M.project I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)

@[simp]

theorem Matroid.project_empty {α : Type u_1} (M : Matroid α) : M.project ∅ = M

theorem Matroid.Indep.of_project {α : Type u_1} {M : Matroid α} {I C : Set α} (hI : (M.project C).Indep I) : M.Indep I

theorem Matroid.Spanning.project_eq {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Spanning X) : M.project X = loopyOn M.E

@[simp]

theorem Matroid.project_ground_self {α : Type u_1} (M : Matroid α) : M.project M.E = loopyOn M.E

@[simp]

theorem Matroid.project_project {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α) : (M.project C₁).project C₂ = M.project (C₁ ∪ C₂)

theorem Matroid.Indep.of_project_subset {α : Type u_1} {M : Matroid α} {I C C' : Set α} (hI : (M.project C).Indep I) (hC' : C' ⊆ C) : (M.project C').Indep I

@[simp]

theorem Matroid.project_delete_self {α : Type u_1} (M : Matroid α) (C : Set α) : (M.project C).delete C = M.contract C

@[simp]

theorem Matroid.project_loops {α : Type u_1} (M : Matroid α) (C : Set α) : (M.project C).loops = M.closure C

@[simp]

theorem Matroid.project_spanning_iff {α : Type u_1} {M : Matroid α} {X C : Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.project C).Spanning X ↔ M.Spanning (X ∪ C)

theorem Matroid.IsBasis'.project_eq_project {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) : M.project X = M.project I

@[simp]

theorem Matroid.project_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} : (M.project X).IsLoop e ↔ e ∈ M.closure X

theorem Matroid.project_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} : (M.project X).IsNonloop e ↔ e ∉ M.closure X ∧ e ∈ M.E

theorem Matroid.IsBasis.project_eq_project {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) : M.project X = M.project I

theorem Matroid.project_isBasis'_eq {α : Type u_1} {M : Matroid α} {C : Set α} : (M.project C).IsBasis' = (M.contract C).IsBasis'

theorem Matroid.project_isBasis_iff {α : Type u_1} {M : Matroid α} {I C X : Set α} (hdj : Disjoint X C) : (M.project C).IsBasis I X ↔ (M.contract C).IsBasis I X

theorem Matroid.project_isBase_eq {α : Type u_1} {M : Matroid α} {C : Set α} : (M.project C).IsBase = (M.contract C).IsBase

@[simp]

theorem Matroid.project_closure_eq {α : Type u_1} (M : Matroid α) (X : Set α) : M.project (M.closure X) = M.project X

@[simp]

theorem Matroid.project_loops_eq {α : Type u_1} (M : Matroid α) : M.project M.loops = M

theorem Matroid.project_eq_self {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.loops) : M.project X = M

theorem Matroid.project_project_eq_project {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.closure X ⊆ M.closure Y) : (M.project X).project Y = M.project Y

theorem Matroid.project_restrict_comm {α : Type u_1} {R X : Set α} (M : Matroid α) (hXR : X ⊆ R) : (M.restrict R).project X = (M.project X).restrict R

theorem Matroid.project_restrict_univ {α : Type u_1} {X : Set α} (M : Matroid α) : (M.restrict Set.univ).project X = (M.project X).restrict Set.univ

theorem Matroid.contract_restrict_univ {α : Type u_1} {X : Set α} (M : Matroid α) : (M.contract X).restrict Set.univ = (M.project X).restrict Set.univ

instance Matroid.project_finitary {α : Type u_1} {M : Matroid α} {X : Set α} [M.Finitary] : (M.project X).Finitary

theorem Matroid.project_comap_image {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) (C : Set α) : (M.project (f '' C)).comap f = (M.comap f).project C

theorem Matroid.project_comap {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) (C : Set β) (hC : C ⊆ Set.range f) : (M.project C).comap f = (M.comap f).project (f ⁻¹' C)

theorem Matroid.Dep.project {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) (C : Set α) : (M.project C).Dep D

theorem Matroid.Indep.project_isBasis'_iff {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Indep I) : (M.project I).IsBasis' J X ↔ M.IsBasis' (I ∪ J) (I ∪ X) ∧ Disjoint I J

theorem Matroid.Indep.project_isBasis_iff {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Indep I) : (M.project I).IsBasis J X ↔ M.IsBasis (I ∪ J) (I ∪ X) ∧ Disjoint I J

theorem Matroid.project_isBasis'_iff_contract_isBasis' {α : Type u_1} {M : Matroid α} {I C X : Set α} : (M.project C).IsBasis' I X ↔ (M.contract C).IsBasis' I (X \ C)

theorem Matroid.project_isFlat_iff {α : Type u_1} {M : Matroid α} {C F : Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.project C).IsFlat F ↔ M.IsFlat F ∧ C ⊆ F

theorem Matroid.project_isFlat_iff' {α : Type u_1} {M : Matroid α} {C F : Set α} : (M.project C).IsFlat F ↔ M.IsFlat F ∧ C ∩ M.E ⊆ F

def Matroid.loopify {α : Type u_1} (M : Matroid α) (D : Set α) : Matroid α

Turn the elements of D into loops.

Equations

• M.loopify D = (M.delete D).restrict M.E

@[simp]

theorem Matroid.loopify_ground {α : Type u_1} (M : Matroid α) (D : Set α) : (M.loopify D).E = M.E

@[simp]

theorem Matroid.loopify_inter_ground {α : Type u_1} (M : Matroid α) (D : Set α) : M.loopify (D ∩ M.E) = M.loopify D

theorem Matroid.loopify_closure {α : Type u_1} {X : Set α} (M : Matroid α) (D : Set α) : (M.loopify D).closure X = M.closure (X \ D) ∪ D ∩ M.E

theorem Matroid.loopify_indep_iff_delete_indep {α : Type u_1} {M : Matroid α} {I D : Set α} : (M.loopify D).Indep I ↔ (M.delete D).Indep I

theorem Matroid.loopify_indep_iff {α : Type u_1} {M : Matroid α} {I D : Set α} : (M.loopify D).Indep I ↔ M.Indep I ∧ Disjoint I D

@[simp]

theorem Matroid.loopify_delete {α : Type u_1} (M : Matroid α) (D : Set α) : (M.loopify D).delete D = M.delete D

theorem Matroid.loopify_eq_loopify_iff {α : Type u_1} {M N : Matroid α} {D : Set α} : M.loopify D = N.loopify D ↔ M.E = N.E ∧ M.delete D = N.delete D

theorem Matroid.IsBasis'.project_eq_loopify_project {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis' I X) : M.project X = (M.loopify (X \ I)).project I

theorem Matroid.IsBasis.project_eq_loopify_project {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) : M.project X = (M.loopify (X \ I)).project I

@[simp]

theorem Matroid.loopify_loopify {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.loopify X).loopify Y = M.loopify (X ∪ Y)

theorem Matroid.loopify_loops_subset {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ (M.loopify X).loops

@[simp]

theorem Matroid.loopify_eq_self_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.loopify X = M ↔ X ⊆ M.loops