theorem Matroid.contract_delete_ground {α : Type u_1} (M : Matroid α) (C D : Set α) : ((M.contract C).delete D).E = M.E \ (C ∪ D)

theorem Matroid.delete_contract_ground {α : Type u_1} (M : Matroid α) (C D : Set α) : ((M.delete D).contract C).E = M.E \ (D ∪ C)

theorem Matroid.IsMinor.exists_contract_indep_delete_coindep {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : ∃ (C : Set α) (D : Set α), M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ N = (M.contract C).delete D

The scum theorem : we can always realize a minor by contracting an independent set and deleting a coindependent set/

theorem Matroid.IsMinor.exists_delete_coindep_contract_indep {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : ∃ (D : Set α) (C : Set α), M.Coindep D ∧ M.Indep C ∧ Disjoint D C ∧ N = (M.delete D).contract C

theorem Matroid.IsMinor.exists_spanning_isRestriction_contract {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : ∃ (C : Set α), M.Indep C ∧ N.IsRestriction (M.contract C) ∧ (M.contract C).closure N.E = (M.contract C).E

A version of the scum theorem where the minor is obtained as a spanning restriction of a contraction rather than a contraction-deletion.

theorem Matroid.IsMinor.exists_eq_contract_spanning_restrict {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : ∃ (I : Set α) (R : Set α), M.Indep I ∧ Disjoint I R ∧ (M.contract I).Spanning R ∧ N = (M.contract I).restrict R

A version of the scum theorem where the minor is obtained as a spanning restriction of a contraction rather than a contraction-deletion.

theorem Matroid.IsRestriction.isMinor {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) : N ≤m M

theorem Matroid.IsMinor.finite {α : Type u_1} {M N : Matroid α} (h : N ≤m M) [M.Finite] : N.Finite

theorem Matroid.IsMinor.rankFinite {α : Type u_1} {M N : Matroid α} (h : N ≤m M) [M.RankFinite] : N.RankFinite

theorem Matroid.IsMinor.finitary {α : Type u_1} {M N : Matroid α} (h : N ≤m M) [M.Finitary] : N.Finitary

theorem Matroid.contract_isMinor {α : Type u_1} (M : Matroid α) (C : Set α) : M.contract C ≤m M

theorem Matroid.contract_isMinor_of_subset {α : Type u_1} (M : Matroid α) {C C' : Set α} (hCC' : C ⊆ C') : M.contract C' ≤m M.contract C

theorem Matroid.contract_isMinor_of_mem {α : Type u_1} {e : α} (M : Matroid α) {C : Set α} (he : e ∈ C) : M.contract C ≤m M.contract {e}

theorem Matroid.delete_isMinor {α : Type u_1} (M : Matroid α) (D : Set α) : M.delete D ≤m M

theorem Matroid.delete_isRestriction_of_subset {α : Type u_1} (M : Matroid α) {D D' : Set α} (hDD' : D ⊆ D') : (M.delete D').IsRestriction (M.delete D)

theorem Matroid.delete_contract_diff {α : Type u_1} (M : Matroid α) (C D : Set α) : (M.delete D).contract C = (M.delete D).contract (C \ D)

theorem Matroid.IsMinor.delete_isMinor_delete {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {D : Set α} (hD : D ⊆ N.E) : N.delete D ≤m M.delete D

theorem Matroid.IsMinor.delete_isMinor_delete' {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {D : Set α} (hD : D ∩ M.E ⊆ N.E) : N.delete D ≤m M.delete D

theorem Matroid.IsMinor.delete_isMinor_delete_of_subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {D D' : Set α} (hss : D ⊆ D') (hD : D ∩ M.E ⊆ N.E) : N.delete D' ≤m M.delete D

theorem Matroid.delete_isMinor_delete_of_subset {α : Type u_1} {D D' : Set α} (M : Matroid α) (hDD' : D ⊆ D') : M.delete D' ≤m M.delete D

theorem Matroid.restrict_isMinor {α : Type u_1} {R : Set α} (M : Matroid α) (hR : R ⊆ M.E := by aesop_mat) : M.restrict R ≤m M

theorem Matroid.Dep.of_isMinor_of_subset {α : Type u_1} {M N : Matroid α} {X : Set α} (hX : M.Dep X) (hNM : N ≤m M) (hIN : X ⊆ N.E) : N.Dep X

theorem Matroid.IsRestriction.isRestriction_left_of_isMinor_isMinor {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) {N' : Matroid α} (hNN' : N ≤m N') (hN'M : N' ≤m M) : N.IsRestriction N'

The right version of this is false; for instance, if N is a component of M, and N' = M ／ C for some set C in another component.

theorem Matroid.IsStrictRestriction.isStrictMinor {α : Type u_1} {M N : Matroid α} (h : N.IsStrictRestriction M) : N <m M

theorem Matroid.restrict_isStrictMinor {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R ⊂ M.E) : M.restrict R <m M

@[simp]

theorem Matroid.delete_contract_isMinor {α : Type u_1} (M : Matroid α) (D C : Set α) : (M.delete D).contract C ≤m M

theorem Matroid.contract_delete_isMinor_delete {α : Type u_1} {C D : Set α} (M : Matroid α) (hCD : Disjoint C D) : (M.contract C).delete D ≤m M.delete D

theorem Matroid.contract_restrict_isMinor {α : Type u_1} {R : Set α} (M : Matroid α) (C : Set α) (hR : R ⊆ M.E \ C) : (M.contract C).restrict R ≤m M

theorem Matroid.contract_delete_isMinor_contract_delete {α : Type u_1} {C D : Set α} (M : Matroid α) {C' D' : Set α} (hCD : Disjoint C D) (hC : C' ⊆ C) (hD : D' ⊆ D) : (M.contract C).delete D ≤m (M.contract C').delete D'

theorem Matroid.IsMinor.exists_isMinor_of_subset_subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {X : Set α} (hNX : N.E ⊆ X) (hXM : X ⊆ M.E) : ∃ (N' : Matroid α), N ≤m N' ∧ N' ≤m M ∧ N'.E = X

theorem Matroid.contractElem_isStrictMinor {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E) : M.contract {e} <m M

theorem Matroid.deleteElem_isStrictMinor {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E) : M.delete {e} <m M

theorem Matroid.IsStrictMinor.exists_eq_contract_delete_disjoint {α : Type u_1} {M N : Matroid α} (hNM : N <m M) : ∃ (C : Set α) (D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = (M.contract C).delete D

theorem Matroid.isStrictMinor_iff_exists_eq_contract_delete {α : Type u_1} {M N : Matroid α} : N <m M ↔ ∃ (C : Set α) (D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = (M.contract C).delete D

theorem Matroid.IsStrictMinor.exists_isMinor_contractElem_or_deleteElem {α : Type u_1} {M N : Matroid α} (hNM : N <m M) : ∃ e ∈ M.E, N ≤m M.contract {e} ∨ N ≤m M.delete {e}

theorem Matroid.IsMinor.isStrictMinor_or_eq {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : N <m M ∨ N = M

theorem Matroid.IsMinor.dual {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : N✶ ≤m M✶

theorem Matroid.IsMinor.of_dual {α : Type u_1} {M N : Matroid α} (h : N✶ ≤m M✶) : N ≤m M

@[simp]

theorem Matroid.dual_isMinor_iff {α : Type u_1} {M N : Matroid α} : N✶ ≤m M✶ ↔ N ≤m M

theorem Matroid.isMinor_dual_iff_dual_isMinor {α : Type u_1} {M N : Matroid α} : N ≤m M✶ ↔ N✶ ≤m M

theorem Matroid.IsStrictMinor.dual {α : Type u_1} {M N : Matroid α} (h : N <m M) : N✶ <m M✶

theorem Matroid.IsStrictMinor.of_dual {α : Type u_1} {M N : Matroid α} (h : N✶ <m M✶) : N <m M

theorem Matroid.dual_isStrictMinor_iff {α : Type u_1} {M N : Matroid α} : N✶ <m M✶ ↔ N <m M

theorem Matroid.isStrictMinor_dual_iff_dual_isStrictMinor {α : Type u_1} {M N : Matroid α} : N <m M✶ ↔ N✶ <m M

theorem Matroid.IsMinor.contract_isMinor_contract {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {C : Set α} (hC : C ⊆ N.E) : N.contract C ≤m M.contract C

theorem Matroid.IsMinor.contract_isMinor_contract' {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {C : Set α} (hC : C ∩ M.E ⊆ N.E) : N.contract C ≤m M.contract C

theorem Matroid.IsMinor.contract_isMinor_contract_of_subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) {C C' : Set α} (hss : C ⊆ C') (hC : C ∩ M.E ⊆ N.E) : N.contract C' ≤m M.contract C

theorem Matroid.IsColoop.of_isMinor {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsColoop e) (heN : e ∈ N.E) (hNM : N ≤m M) : N.IsColoop e

theorem Matroid.IsStrictMinor.encard_ground_lt {α : Type u_1} {M N : Matroid α} [N.Finite] (hNM : N <m M) : N.E.encard < M.E.encard

theorem Matroid.Nonspanning.of_isMinor {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N.Nonspanning X) (hN : N ≤m M) : M.Nonspanning X

theorem Matroid.IsMinor.closure_inter_subset_closure {α : Type u_1} {M N : Matroid α} {X : Set α} (hN : N ≤m M) (hX : X ⊆ N.E) : M.closure X ∩ N.E ⊆ N.closure X

theorem Matroid.Spanning.of_isMinor {α : Type u_1} {M N : Matroid α} {X : Set α} (hX : M.Spanning X) (hN : N ≤m M) (hXN : X ⊆ N.E) : N.Spanning X

theorem Matroid.IsSpanningRestriction.isMinor {α : Type u_1} {M N : Matroid α} (h : N.IsSpanningRestriction M) : N ≤m M

theorem Matroid.IsMinor.isSpanningRestriction_of_indep_spanning {α : Type u_1} {M N : Matroid α} {X : Set α} (hNM : N ≤m M) (hNX : N.Indep X) (hMX : M.Spanning X) : N.IsSpanningRestriction M

If X is spanning in M, and independent in a minor N of M, then N is a spanning restriction of M.

theorem Matroid.IsSpanningRestriction.isSpanningRestriction_left_of_isMinor_isMinor {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁.IsSpanningRestriction M₃) (h₁₂ : M₁ ≤m M₂) (h₂₃ : M₂ ≤m M₃) : M₁.IsSpanningRestriction M₂

theorem Matroid.IsSpanningRestriction.isSpanningRestriction_right_of_isMinor_isMinor {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁.IsSpanningRestriction M₃) (h₁₂ : M₁ ≤m M₂) (h₂₃ : M₂ ≤m M₃) : M₂.IsSpanningRestriction M₃

theorem Matroid.finite_setOf_isMinor {α : Type u_1} (M : Matroid α) [M.Finite] : {N : Matroid α | N ≤m M}.Finite

@[simp]

theorem Matroid.emptyOn_isMinor {α : Type u_1} (M : Matroid α) : emptyOn α ≤m M

@[simp]

theorem Matroid.isMinor_emptyOn_iff {α : Type u_1} {M : Matroid α} : M ≤m emptyOn α ↔ M = emptyOn α

theorem Matroid.isMinor_loopyOn_iff_exists {α : Type u_1} {M : Matroid α} {E : Set α} : M ≤m loopyOn E ↔ ∃ F ⊆ E, M = loopyOn F

theorem Matroid.isMinor_loopyOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} : M ≤m loopyOn E ↔ M = loopyOn M.E ∧ M.E ⊆ E

@[simp]

theorem Matroid.freeOn_isMinor_iff {α : Type u_1} {M : Matroid α} {E : Set α} : freeOn E ≤m M ↔ M.Indep E

@[simp]

theorem Matroid.loopyOn_isMinor_iff {α : Type u_1} {M : Matroid α} {E : Set α} : loopyOn E ≤m M ↔ M.Coindep E