def Matroid.Iso.delete {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (D : Set α) : M.delete D ≂ N.delete (Subtype.val '' ⇑e '' Subtype.val ⁻¹' D)

Deletions of isomorphic matroids are isomorphic.

Equations

• e.delete D = e.restrict ⋯ ⋯ ⋯

def Matroid.Iso.contract {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (C : Set α) : M.contract C ≂ N.contract (Subtype.val '' ⇑e '' Subtype.val ⁻¹' C)

Contractions of isomorphic matroids are isomorphic.

Equations

• e.contract C = (e.dual.delete C).dual

structure Matroid.IsoRestr {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) : Type (max u_1 u_2)

N ≤ir M means that N is isomorphic to a restriction of M. Defined as a function from N.E to M.E.

• toFun : ↑N.E → ↑M.E
• inj' : Function.Injective self.toFun
• indep_iff' (I : Set ↑N.E) : N.Indep (Subtype.val '' I) ↔ M.Indep (Subtype.val '' self.toFun '' I)

def Matroid.«term_≤ir_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_≤ir_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤ir_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ir ") (Lean.ParserDescr.cat `term 66))

@[instance_reducible]

instance Matroid.instFunLikeIsoRestrElemE {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : FunLike (IsoRestr N M) ↑N.E ↑M.E

Equations

• Matroid.instFunLikeIsoRestrElemE = { coe := fun (f : Matroid.IsoRestr N M) => f.toFun, coe_injective := ⋯ }

instance Matroid.instEmbeddingLikeIsoRestrElemE {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : EmbeddingLike (IsoRestr N M) ↑N.E ↑M.E

theorem Matroid.IsoRestr.indep_image_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoRestr N M) {I : Set ↑N.E} : M.Indep (Subtype.val '' ⇑i '' I) ↔ N.Indep (Subtype.val '' I)

def Matroid.Iso.isoRestr {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : N ≂ M) : IsoRestr N M

Equations

• e.isoRestr = { toFun := ⇑e, inj' := ⋯, indep_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.isoRestr_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : N ≂ M) (x : ↑N.E) : e.isoRestr x = e x

@[simp]

theorem Matroid.Iso.range_isoRestr {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : N ≂ M) : Set.range ⇑e.isoRestr = Set.univ

def Matroid.IsRestriction.isoRestr {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) : IsoRestr N M

Equations

• h.isoRestr = { toFun := Set.inclusion ⋯, inj' := ⋯, indep_iff' := ⋯ }

noncomputable def Matroid.IsoRestr.iso_restrict_range_comp {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoRestr N M) : N ≂ M.restrict (Set.range (Subtype.val ∘ ⇑i))

Equations

• i.iso_restrict_range_comp = { toEquiv := Equiv.ofInjective (Subtype.val ∘ ⇑i) ⋯, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.IsoRestr.iso_restrict_range_comp_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoRestr N M) (e : ↑N.E) : i.iso_restrict_range_comp e = ⟨↑(i e), ⋯⟩

@[simp]

theorem Matroid.IsoRestr.iso_restrict_range_comp_apply_coe {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoRestr N M) (e : ↑N.E) : ↑(i.iso_restrict_range_comp e) = ↑(i e)

theorem Matroid.IsoRestr.exists_restr_iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoRestr N M) : ∃ (M₀ : Matroid α) (e : N ≂ M₀) (hr : M₀.IsRestriction M), Set.inclusion ⋯ ∘ ⇑e = ⇑i

def Matroid.IsoRestr.trans {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i₁ : IsoRestr M₁ M₂) (i₂ : IsoRestr M₂ M₃) : IsoRestr M₁ M₃

≤ir is transitive.

Equations

• i₁.trans i₂ = { toFun := ⇑i₂ ∘ ⇑i₁, inj' := ⋯, indep_iff' := ⋯ }

@[simp]

theorem Matroid.IsoRestr.trans_apply {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i₁ : IsoRestr M₁ M₂) (i₂ : IsoRestr M₂ M₃) (x : ↑M₁.E) : (i₁.trans i₂) x = i₂ (i₁ x)

@[simp]

theorem Matroid.IsoRestr.range_trans {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i₁ : IsoRestr M₁ M₂) (i₂ : IsoRestr M₂ M₃) : Set.range ⇑(i₁.trans i₂) = ⇑i₂ '' Set.range ⇑i₁

def Matroid.IsoRestr.Spanning {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : IsoRestr N M) : Prop

For e : N ≤ir M, e.Spanning N M means that N embeds in M as a spanning restriction.

Equations

• e.Spanning = M.Spanning (Subtype.val '' Set.range ⇑e)

theorem Matroid.IsoRestr.Spanning.exists_restr_iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {i : IsoRestr N M} (hi : i.Spanning) : ∃ (M₀ : Matroid α) (e : N ≂ M₀) (hr : M₀.IsRestriction M), M.Spanning M₀.E ∧ Set.inclusion ⋯ ∘ ⇑e = ⇑i

theorem Matroid.IsoRestr.Spanning.trans {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} {e₁ : IsoRestr M₁ M₂} {e₂ : IsoRestr M₂ M₃} (he₁ : e₁.Spanning) (he₂ : e₂.Spanning) : (e₁.trans e₂).Spanning

def Matroid.IsoRestr.ofSubtypeFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑M.E → β) (hf : Function.Injective f) (hfN : Set.range f ⊆ N.E) (hfI : ∀ (I : Set ↑M.E), M.Indep (Subtype.val '' I) ↔ N.Indep (f '' I)) : IsoRestr M N

Construct an IsoRestr from a function defined on all of α rather than a subtype.

Equations

• Matroid.IsoRestr.ofSubtypeFun f hf hfN hfI = { toFun := fun (e : ↑M.E) => ⟨f e, ⋯⟩, inj' := ⋯, indep_iff' := ⋯ }

@[simp]

theorem Matroid.IsoRestr.ofSubtypeFun_toFun_coe {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑M.E → β) (hf : Function.Injective f) (hfN : Set.range f ⊆ N.E) (hfI : ∀ (I : Set ↑M.E), M.Indep (Subtype.val '' I) ↔ N.Indep (f '' I)) (e : ↑M.E) : ↑((ofSubtypeFun f hf hfN hfI) e) = f e

@[simp]

theorem Matroid.IsoRestr_ofSubtypeFun_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑M.E → β) (hf : Function.Injective f) (hfN : Set.range f ⊆ N.E) (hfI : ∀ (I : Set ↑M.E), M.Indep (Subtype.val '' I) ↔ N.Indep (f '' I)) (e : ↑M.E) : (IsoRestr.ofSubtypeFun f hf hfN hfI) e = ⟨f e, ⋯⟩

theorem Matroid.IsoRestr.ofSubtypeFun_spanning {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑M.E → β) (hf : Function.Injective f) (hfI : ∀ (I : Set ↑M.E), M.Indep (Subtype.val '' I) ↔ N.Indep (f '' I)) (hfs : N.Spanning (Set.range f)) : (ofSubtypeFun f hf ⋯ hfI).Spanning

def Matroid.IsoRestr.ofFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : α → β) (hf : Set.InjOn f M.E) (hfN : f '' M.E ⊆ N.E) (hfI : ∀ I ⊆ M.E, M.Indep I ↔ N.Indep (f '' I)) : IsoRestr M N

Construct an IsoRestr from a function defined on all of α rather than a subtype.

Equations

• Matroid.IsoRestr.ofFun f hf hfN hfI = { toFun := fun (e : ↑M.E) => ⟨f ↑e, ⋯⟩, inj' := ⋯, indep_iff' := ⋯ }

@[simp]

theorem Matroid.IsoRestr.ofFun_toFun_coe {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : α → β) (hf : Set.InjOn f M.E) (hfN : f '' M.E ⊆ N.E) (hfI : ∀ I ⊆ M.E, M.Indep I ↔ N.Indep (f '' I)) (e : ↑M.E) : ↑((ofFun f hf hfN hfI) e) = f ↑e

@[simp]

theorem Matroid.IsoRestr_ofFun_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : α → β) (hf : Set.InjOn f M.E) (hfN : f '' M.E ⊆ N.E) (hfI : ∀ I ⊆ M.E, M.Indep I ↔ N.Indep (f '' I)) (e : ↑M.E) : (IsoRestr.ofFun f hf hfN hfI) e = ⟨f ↑e, ⋯⟩

theorem Matroid.IsoRestr.ofFun_spanning {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : α → β) (hf : Set.InjOn f M.E) (hfI : ∀ I ⊆ M.E, M.Indep I ↔ N.Indep (f '' I)) (hfs : N.Spanning (f '' M.E)) : (ofFun f hf ⋯ hfI).Spanning

theorem Matroid.Iso.isoRestr_spanning {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : N ≂ M) : e.isoRestr.Spanning

def Matroid.IsoRestr.ofEmptyOn {α : Type u_1} {β : Type u_2} (M : Matroid β) : IsoRestr (emptyOn α) M

Equations

• Matroid.IsoRestr.ofEmptyOn M = (Matroid.empty_iso_empty α β).isoRestr.trans ⋯.isoRestr

structure Matroid.IsoMinor {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) : Type (max u_1 u_2)

N ≤i M means that M has an N-minor; i.e. N is isomorphic to a minor of M. The data a term of this type contains is just a function from N.E to M.E rather than a choice of delete and contract-sets, which may not be unique.

• toFun : ↑N.E → ↑M.E
• inj' : Function.Injective self.toFun
• exists_isMinor' : ∃ (M₀ : Matroid α), M₀ ≤m M ∧ M₀.E = Subtype.val '' Set.range self.toFun ∧ ∀ (I : Set ↑N.E), N.Indep (Subtype.val '' I) ↔ M₀.Indep (Subtype.val '' self.toFun '' I)

structure Matroid.StrictIsoMinor {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) : Type (max u_1 u_2)

N <i M means that N can be embeddeded in M as a minor via a function that is not surjective.

• toFun : ↑N.E → ↑M.E
• inj' : Function.Injective self.toFun
• exists_isMinor' : ∃ (M₀ : Matroid α), M₀ ≤m M ∧ M₀.E = Subtype.val '' Set.range self.toFun ∧ ∀ (I : Set ↑N.E), N.Indep (Subtype.val '' I) ↔ M₀.Indep (Subtype.val '' self.toFun '' I)
• not_surj : ¬Function.Surjective self.toFun

def Matroid.«term_≤i_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_≤i_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤i_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤i ") (Lean.ParserDescr.cat `term 66))

def Matroid.«term_<i_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_<i_» = Lean.ParserDescr.trailingNode `Matroid.«term_<i_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <i ") (Lean.ParserDescr.cat `term 66))

@[instance_reducible]

instance Matroid.instFunLikeIsoMinorElemE {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : FunLike (IsoMinor N M) ↑N.E ↑M.E

Equations

• Matroid.instFunLikeIsoMinorElemE = { coe := fun (f : Matroid.IsoMinor N M) => f.toFun, coe_injective := ⋯ }

@[instance_reducible]

instance Matroid.instFunLikeStrictIsoMinorElemE {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : FunLike (StrictIsoMinor N M) ↑N.E ↑M.E

Equations

• Matroid.instFunLikeStrictIsoMinorElemE = { coe := fun (f : Matroid.StrictIsoMinor N M) => f.toFun, coe_injective := ⋯ }

instance Matroid.instEmbeddingLikeIsoMinorElemE {α : Type u_4} {β : Type u_5} {N : Matroid α} {M : Matroid β} : EmbeddingLike (IsoMinor N M) ↑N.E ↑M.E

instance Matroid.instEmbeddingLikeStrictIsoMinorElemE {α : Type u_4} {β : Type u_5} {N : Matroid α} {M : Matroid β} : EmbeddingLike (StrictIsoMinor N M) ↑N.E ↑M.E

def Matroid.StrictIsoMinor.isoMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : StrictIsoMinor N M) : IsoMinor N M

Equations

• e.isoMinor = { toFun := ⇑e, inj' := ⋯, exists_isMinor' := ⋯ }

@[simp]

theorem Matroid.StrictIsoMinor.isoMinor_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : StrictIsoMinor N M) (a : ↑N.E) : e.isoMinor a = e a

theorem Matroid.StrictIsoMinor.not_surjective {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : StrictIsoMinor N M) : ¬Function.Surjective ⇑e

theorem Matroid.IsoMinor.injective {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : IsoMinor N M) : Function.Injective ⇑f

theorem Matroid.IsoMinor.exists_isMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) : ∃ (M₀ : Matroid α), M₀ ≤m M ∧ M₀.E = Subtype.val '' Set.range ⇑i ∧ ∀ (I : Set ↑N.E), N.Indep (Subtype.val '' I) ↔ M₀.Indep (Subtype.val '' ⇑i '' I)

theorem Matroid.StrictIsoMinor.exists_isMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : StrictIsoMinor N M) : ∃ (M₀ : Matroid α), M₀ <m M ∧ M₀.E = Subtype.val '' Set.range ⇑i ∧ ∀ (I : Set ↑N.E), N.Indep (Subtype.val '' I) ↔ M₀.Indep (Subtype.val '' ⇑i '' I)

theorem Matroid.IsoMinor.exists_iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) : ∃ (M₀ : Matroid α) (hM₀ : M₀ ≤m M) (e : N ≂ M₀), ∀ (x : ↑N.E), Set.inclusion ⋯ (e x) = i x

theorem Matroid.StrictIsoMinor.exists_iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : StrictIsoMinor N M) : ∃ (M₀ : Matroid α) (hM₀ : M₀ <m M) (e : N ≂ M₀), ∀ (x : ↑N.E), Set.inclusion ⋯ (e x) = i x

def Matroid.IsoMinor.strictIsoMinor_of_not_surjective {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) (hi : ¬Function.Surjective ⇑i) : StrictIsoMinor N M

Equations

• i.strictIsoMinor_of_not_surjective hi = { toFun := i.toFun, inj' := ⋯, exists_isMinor' := ⋯, not_surj := hi }

@[simp]

theorem Matroid.IsoMinor.strictIsoMinor_of_not_surjective_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) (hi : ¬Function.Surjective ⇑i) (a✝ : ↑N.E) : (i.strictIsoMinor_of_not_surjective hi) a✝ = i.toFun a✝

def Matroid.IsoMinor.ofExistsIso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑N.E → ↑M.E) (h : ∃ (M₀ : Matroid α) (hM₀ : M₀ ≤m M) (e : N ≂ M₀), ∀ (x : ↑N.E), Set.inclusion ⋯ (e x) = f x) : IsoMinor N M

If there is an isomorphism from N to a isMinor M₀ of M, then N ≤i M.

Equations

• Matroid.IsoMinor.ofExistsIso f h = { toFun := f, inj' := ⋯, exists_isMinor' := ⋯ }

@[simp]

theorem Matroid.IsoMinor.ofExistsIso_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑N.E → ↑M.E) (h : ∃ (M₀ : Matroid α) (hM₀ : M₀ ≤m M) (e : N ≂ M₀), ∀ (x : ↑N.E), Set.inclusion ⋯ (e x) = f x) (a✝ : ↑N.E) : (ofExistsIso f h) a✝ = f a✝

def Matroid.Iso.transIsMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {M₀ : Matroid α} (e : N ≂ M₀) (hM₀ : M₀ ≤m M) : IsoMinor N M

If N ≂ M₀ and M₀ ≤m M then N ≤i M.

Equations

• e.transIsMinor hM₀ = { toFun := fun (x : ↑N.E) => Set.inclusion ⋯ (e x), inj' := ⋯, exists_isMinor' := ⋯ }

@[simp]

theorem Matroid.Iso.transIsMinor_toFun_coe {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {M₀ : Matroid α} (e : N ≂ M₀) (hM₀ : M₀ ≤m M) (x : ↑N.E) : ↑((e.transIsMinor hM₀) x) = ↑(e x)

def Matroid.Iso.isoMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : IsoMinor M N

If M and N are isomorphic, then M ≤i N.

Equations

• e.isoMinor = Matroid.IsoMinor.ofExistsIso ⇑e ⋯

@[simp]

theorem Matroid.Iso.isoMinor_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (a : ↑M.E) : e.isoMinor a = e a

def Matroid.IsMinor.isoMinor {α : Type u_1} {M N : Matroid α} (h : M ≤m N) : IsoMinor M N

If M ≤m N, then M ≤i M.

Equations

• h.isoMinor = Matroid.IsoMinor.ofExistsIso (Set.inclusion ⋯) ⋯

@[simp]

theorem Matroid.IsMinor.isoMinor_toFun_coe {α : Type u_1} {M N : Matroid α} (h : M ≤m N) (a✝ : ↑M.E) : ↑(h.isoMinor a✝) = ↑a✝

def Matroid.IsoMinor.dual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) : IsoMinor N✶ M✶

If N ≤i M then N✶ ≤i M✶.

Equations

• i.dual = Matroid.IsoMinor.ofExistsIso ⇑i ⋯

@[simp]

theorem Matroid.IsoMinor.dual_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) (a : ↑N.E) : i.dual a = i a

def Matroid.StrictIsoMinor.dual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : StrictIsoMinor N M) : StrictIsoMinor N✶ M✶

Equations

• e.dual = e.isoMinor.dual.strictIsoMinor_of_not_surjective ⋯

@[simp]

theorem Matroid.StrictIsoMinor.dual_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : StrictIsoMinor N M) (a✝ : ↑N✶.E) : e.dual a✝ = e.isoMinor.dual.toFun a✝

def Matroid.IsoMinor.bDual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : IsoMinor N M) (b : Bool) : IsoMinor (N.bDual b) (M.bDual b)

Equations

• i.bDual true = i.dual
• i.bDual false = i

def Matroid.StrictIsoMinor.bDual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : StrictIsoMinor N M) (b : Bool) : StrictIsoMinor (N.bDual b) (M.bDual b)

Equations

• i.bDual true = i.dual
• i.bDual false = i

def Matroid.IsoMinor.trans_iso {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i : IsoMinor M₁ M₂) (e : M₂ ≂ M₃) : IsoMinor M₁ M₃

If M₁ ≤i M₂ and M₂ ≂ M₃ then M₁ ≤i M₃.

Equations

• i.trans_iso e = Matroid.IsoMinor.ofExistsIso (⇑e ∘ ⇑i) ⋯

def Matroid.IsoMinor.trans_isMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {M' : Matroid α} (i : IsoMinor N M) (hM : M ≤m M') : IsoMinor N M'

If M₁ ≤i M₂ and M₂ ≤m M₃ then M₁ ≤i M₃.

Equations

• i.trans_isMinor hM = { toFun := Set.inclusion ⋯ ∘ ⇑i, inj' := ⋯, exists_isMinor' := ⋯ }

def Matroid.IsoMinor.congr_exists {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑N.E → ↑M.E) (h : ∃ (i : IsoMinor N M), ∀ (x : ↑N.E), i x = f x) : IsoMinor N M

Construct a term N ≤i M from an explicitly given embedding and an existence proof. Useful for computability and defeq.

Equations

• Matroid.IsoMinor.congr_exists f h = { toFun := f, inj' := ⋯, exists_isMinor' := ⋯ }

@[simp]

theorem Matroid.IsoMinor.congr_exists_toFun {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (f : ↑N.E → ↑M.E) (h : ∃ (i : IsoMinor N M), ∀ (x : ↑N.E), i x = f x) (a✝ : ↑N.E) : (congr_exists f h) a✝ = f a✝

def Matroid.IsoMinor.trans {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i₁ : IsoMinor M₁ M₂) (i₂ : IsoMinor M₂ M₃) : IsoMinor M₁ M₃

≤i is transitive.

Equations

• i₁.trans i₂ = Matroid.IsoMinor.congr_exists (⇑i₂ ∘ ⇑i₁) ⋯

@[simp]

theorem Matroid.IsoMinor.trans_toFun {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i₁ : IsoMinor M₁ M₂) (i₂ : IsoMinor M₂ M₃) (a✝ : ↑M₁.E) : (i₁.trans i₂) a✝ = i₂ (i₁ a✝)

def Matroid.IsoMinor.ofDual {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) (i : IsoMinor N✶ M✶) : IsoMinor N M

Equations

• Matroid.IsoMinor.ofDual N M i = ((Matroid.Iso.ofEq ⋯).symm.isoMinor.trans i.dual).trans (Matroid.Iso.ofEq ⋯).isoMinor

@[simp]

theorem Matroid.IsoMinor.ofDual_toFun_coe {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) (i : IsoMinor N✶ M✶) (a✝ : ↑N.E) : ↑((ofDual N M i) a✝) = ↑(((Iso.ofEq ⋯).symm.isoMinor.trans i.dual) a✝)

def Matroid.StrictIsoMinor.ofDual {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) (i : StrictIsoMinor N✶ M✶) : StrictIsoMinor N M

Equations

• Matroid.StrictIsoMinor.ofDual N M i = (Matroid.IsoMinor.ofDual N M i.isoMinor).strictIsoMinor_of_not_surjective ⋯

@[simp]

theorem Matroid.StrictIsoMinor.ofDual_toFun_coe {α : Type u_1} {β : Type u_2} (N : Matroid β) (M : Matroid α) (i : StrictIsoMinor N✶ M✶) (a✝ : ↑N.E) : ↑((ofDual N M i) a✝) = ↑(((Iso.ofEq ⋯).symm.isoMinor.trans i.isoMinor.dual) a✝)

def Matroid.IsoMinor.ofbDual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {b : Bool} (i : IsoMinor (N.bDual b) (M.bDual b)) : IsoMinor N M

Equations

• i_2.ofbDual = Matroid.IsoMinor.ofDual N M i_2
• i_2.ofbDual = i_2

def Matroid.StrictIsoMinor.ofbDual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {b : Bool} (i : StrictIsoMinor (N.bDual b) (M.bDual b)) : StrictIsoMinor N M

Equations

• i_2.ofbDual = Matroid.StrictIsoMinor.ofDual N M i_2
• i_2.ofbDual = i_2

@[simp]

theorem Matroid.nonempty_isoMinor_dual_iff {α : Type u_1} {β : Type u_2} {N : Matroid β} {M : Matroid α} : Nonempty (IsoMinor N✶ M✶) ↔ Nonempty (IsoMinor N M)

@[simp]

theorem Matroid.nonempty_strictIsoMinor_dual_iff {α : Type u_1} {β : Type u_2} {N : Matroid β} {M : Matroid α} : Nonempty (StrictIsoMinor N✶ M✶) ↔ Nonempty (StrictIsoMinor N M)

@[simp]

theorem Matroid.nonempty_isoMinor_bDual_iff {α : Type u_1} {β : Type u_2} {N : Matroid β} {M : Matroid α} (b : Bool) : Nonempty (IsoMinor (N.bDual b) (M.bDual b)) ↔ Nonempty (IsoMinor N M)

@[simp]

theorem Matroid.nonempty_strictIsoMinor_bDual_iff {α : Type u_1} {β : Type u_2} {N : Matroid β} {M : Matroid α} (b : Bool) : Nonempty (StrictIsoMinor (N.bDual b) (M.bDual b)) ↔ Nonempty (StrictIsoMinor N M)

theorem Matroid.nonempty_isoMinor_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : Nonempty (IsoMinor N M) ↔ ∃ (M₀ : Matroid α), M₀ ≤m M ∧ Nonempty (N ≂ M₀)

def Matroid.IsoMinor.trans_strictIsoMinor {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i : IsoMinor M₁ M₂) (i' : StrictIsoMinor M₂ M₃) : StrictIsoMinor M₁ M₃

Equations

• i.trans_strictIsoMinor i' = (i.trans i'.isoMinor).strictIsoMinor_of_not_surjective ⋯

@[simp]

theorem Matroid.IsoMinor.trans_strictIsoMinor_toFun {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i : IsoMinor M₁ M₂) (i' : StrictIsoMinor M₂ M₃) (a✝ : ↑M₁.E) : (i.trans_strictIsoMinor i') a✝ = (i.trans i'.isoMinor).toFun a✝

def Matroid.StrictIsoMinor.trans_isoMinor {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i : StrictIsoMinor M₁ M₂) (i' : IsoMinor M₂ M₃) : StrictIsoMinor M₁ M₃

Equations

• i.trans_isoMinor i' = (i.isoMinor.trans i').strictIsoMinor_of_not_surjective ⋯

@[simp]

theorem Matroid.StrictIsoMinor.trans_isoMinor_toFun {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {M₁ : Matroid α₁} {M₂ : Matroid α₂} {M₃ : Matroid α₃} (i : StrictIsoMinor M₁ M₂) (i' : IsoMinor M₂ M₃) (a✝ : ↑M₁.E) : (i.trans_isoMinor i') a✝ = (i.isoMinor.trans i').toFun a✝

def Matroid.emptyOn_isoMinor {β : Type u_2} (α : Type u_4) (M : Matroid β) : IsoMinor (emptyOn α) M

Equations

• Matroid.emptyOn_isoMinor α M = { toFun := ⋯.elim', inj' := ⋯, exists_isMinor' := ⋯ }

@[simp]

theorem Matroid.nonempty_emptyOn_isoMinor {β : Type u_4} (M : Matroid β) (α : Type u_5) : Nonempty (IsoMinor (emptyOn α) M)

noncomputable def Matroid.IsoRestr.isoMinor {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : IsoRestr N M) : IsoMinor N M

Equations

• e.isoMinor = ⋯.choose.isoMinor.trans ⋯.isoMinor

theorem Matroid.IsoMinor.eRank_le {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : IsoMinor N M) : N.eRank ≤ M.eRank

theorem Matroid.IsoMinor.rank_le {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : IsoMinor N M) [M.RankFinite] : N.rank ≤ M.rank

theorem Matroid.IsoMinor.encard_ground_le {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : IsoMinor N M) : N.E.encard ≤ M.E.encard

theorem Matroid.StrictIsoMinor.encard_ground_lt {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : StrictIsoMinor N M) (hN : N.Finite) : N.E.encard < M.E.encard

structure Matroid.IsDeletableSet {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) (D : Set α) : Prop

• subset_ground : D ⊆ M.E
• has_minor : Nonempty (IsoMinor N (M.delete D))

structure Matroid.IsContractibleSet {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) (C : Set α) : Prop

• subset_ground : C ⊆ M.E
• has_minor : Nonempty (IsoMinor N (M.contract C))

@[reducible, inline]

abbrev Matroid.IsDeletable {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) (e : α) : Prop

Equations

• M.IsDeletable N e = M.IsDeletableSet N {e}

@[reducible, inline]

abbrev Matroid.IsContractible {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) (e : α) : Prop

Equations

• M.IsContractible N e = M.IsContractibleSet N {e}

theorem Matroid.IsDeletable.mem_ground {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} (h : M.IsDeletable N e) : e ∈ M.E

theorem Matroid.IsContractible.mem_ground {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} (h : M.IsContractible N e) : e ∈ M.E

theorem Matroid.IsDeletableSet.isContractibleSet_dual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {X : Set α} (h : M.IsDeletableSet N X) : M✶.IsContractibleSet N✶ X

theorem Matroid.IsContractibleSet.isDeletableSet_dual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {X : Set α} (h : M.IsContractibleSet N X) : M✶.IsDeletableSet N✶ X

theorem Matroid.isDeletableSet_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {X : Set α} : M✶.IsDeletableSet N X ↔ M.IsContractibleSet N✶ X

theorem Matroid.isContractibleSet_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {X : Set α} : M✶.IsContractibleSet N X ↔ M.IsDeletableSet N✶ X

@[simp]

theorem Matroid.dual_isDeletableSet_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {X : Set α} : M✶.IsDeletableSet N✶ X ↔ M.IsContractibleSet N X

@[simp]

theorem Matroid.dual_isContractibleSet_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {X : Set α} : M✶.IsContractibleSet N✶ X ↔ M.IsDeletableSet N X

theorem Matroid.isDeletable_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} : M✶.IsDeletable N e ↔ M.IsContractible N✶ e

theorem Matroid.isContractible_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} : M✶.IsContractible N e ↔ M.IsDeletable N✶ e

@[simp]

theorem Matroid.dual_isDeletable_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} : M✶.IsDeletable N✶ e ↔ M.IsContractible N e

@[simp]

theorem Matroid.dual_isContractible_dual_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} : M✶.IsContractible N✶ e ↔ M.IsDeletable N e

theorem Matroid.IsContractible.dual_isDeletable {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} : M.IsDeletable N e → M✶.IsContractible N✶ e

Alias of the reverse direction of Matroid.dual_isContractible_dual_iff.

theorem Matroid.IsDeletable.dual_isContractible {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} {e : α} : M.IsContractible N e → M✶.IsDeletable N✶ e

Alias of the reverse direction of Matroid.dual_isDeletable_dual_iff.

theorem Matroid.StrictIsoMinor.exists_isDeletable_or_isContractible {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : StrictIsoMinor N M) : ∃ (e : α), M.IsContractible N e ∨ M.IsDeletable N e

theorem Matroid.freeOn_isoMinor_iff {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} : Nonempty (IsoMinor (freeOn E) M) ↔ ∃ (f : ↑E ↪ β), M.Indep (Set.range ⇑f)

theorem Matroid.freeOn_isoMinor_iff_of_finite {α : Type u_1} {M : Matroid α} {E : Set α} (hE : E.Finite) : Nonempty (IsoMinor (freeOn E) M) ↔ E.encard ≤ M.eRank