def Matroid.ModularCut.ExtIndep {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (e : α) (I : Set α) : Prop

U.ExtIndep e I means that I is independent in the matroid obtained from M by adding an element e using U, so either I is independent not containing e, or I = insert e J for some M-independent set J whose closure isn't in U.

Equations

• U.ExtIndep e I = (M.Indep I ∧ e ∉ I ∨ M.Indep (I \ {e}) ∧ M.closure (I \ {e}) ∉ U ∧ e ∈ I)

theorem Matroid.ModularCut.extIndep_iff_of_notMem {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {U : M.ModularCut} (heI : e ∉ I) : U.ExtIndep e I ↔ M.Indep I

theorem Matroid.Indep.extIndep {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {U : M.ModularCut} (hI : M.Indep I) (he : e ∉ M.E) : U.ExtIndep e I

theorem Matroid.ModularCut.extIndep_iff_of_mem {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {U : M.ModularCut} (heI : e ∈ I) : U.ExtIndep e I ↔ M.Indep (I \ {e}) ∧ M.closure (I \ {e}) ∉ U

theorem Matroid.ModularCut.ExtIndep.sdiff_singleton_indep {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {U : M.ModularCut} (h : U.ExtIndep e I) : M.Indep (I \ {e})

theorem Matroid.ModularCut.ExtIndep.subset {α : Type u_1} {M : Matroid α} {I J : Set α} {e : α} {U : M.ModularCut} (h : U.ExtIndep e I) (hJI : J ⊆ I) : U.ExtIndep e J

theorem Matroid.ModularCut.ExtIndep.subset_insert_ground {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {U : M.ModularCut} (h : U.ExtIndep e I) : I ⊆ insert e M.E

theorem Matroid.ModularCut.extIndep_aug {α : Type u_1} {M : Matroid α} {I B : Set α} {e : α} {U : M.ModularCut} (hI : U.ExtIndep e I) (hInmax : ¬Maximal (U.ExtIndep e) I) (hBmax : Maximal (U.ExtIndep e) B) : ∃ x ∈ B \ I, U.ExtIndep e (insert x I)

theorem Matroid.ModularCut.existsMaximalSubsetProperty {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (hXE : X ⊆ insert e M.E) : ExistsMaximalSubsetProperty (U.ExtIndep e) X

def Matroid.extendBy {α : Type u_1} (M : Matroid α) (e : α) (U : M.ModularCut) : Matroid α

Extend a matroid M by a new element e using a modular cut U. (If e already belongs to M, then this deletes the existing element e first.)

Equations

• M.extendBy e U = { E := insert e M.E, Indep := U.ExtIndep e, indep_empty := ⋯, indep_subset := ⋯, indep_aug := ⋯, indep_maximal := ⋯, subset_ground := ⋯ }.matroid

@[simp]

theorem Matroid.extendBy_IsBase {α : Type u_1} (M : Matroid α) (e : α) (U : M.ModularCut) (x : Set α) : (M.extendBy e U).IsBase x = Maximal (U.ExtIndep e) x

@[simp]

theorem Matroid.extendBy_E {α : Type u_1} (M : Matroid α) (e : α) (U : M.ModularCut) : (M.extendBy e U).E = insert e M.E

@[simp]

theorem Matroid.extendBy_Indep {α : Type u_1} (M : Matroid α) (e : α) (U : M.ModularCut) (a✝ : Set α) : (M.extendBy e U).Indep a✝ = U.ExtIndep e a✝

@[simp]

theorem Matroid.extendBy_ground {α : Type u_1} (M : Matroid α) (e : α) (U : M.ModularCut) : (M.extendBy e U).E = insert e M.E

theorem Matroid.ModularCut.deleteElem_extendBy {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E) : (M.delete {e}).extendBy e (ofDeleteElem M e) = M

theorem Matroid.ModularCut.extendBy_deleteElem {α : Type u_1} {M : Matroid α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) : (M.extendBy e U).delete {e} = M

theorem Matroid.ModularCut.extendBy_deleteElem' {α : Type u_1} {M : Matroid α} {e : α} (U : M.ModularCut) : (M.extendBy e U).delete {e} = M.delete {e}

theorem Matroid.ModularCut.isRestriction_extendBy {α : Type u_1} {M : Matroid α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) : M.IsRestriction (M.extendBy e U)

theorem Matroid.ModularCut.eq_extendBy_of_forall_flat {α : Type u_1} {M : Matroid α} {e : α} (𝓕 : (M.delete {e}).ModularCut) (he : e ∈ M.E) (h_flat : ∀ ⦃F : Set α⦄, (M.delete {e}).IsFlat F → (e ∈ M.closure F ↔ F ∈ 𝓕)) : (M.delete {e}).extendBy e 𝓕 = M

theorem Matroid.ModularCut.extendBy_injective {α : Type u_1} {e : α} (M : Matroid α) (he : e ∉ M.E) : Function.Injective (M.extendBy e)

Different modular cuts give different extensions.

def Matroid.ModularCut.equivExtension {α : Type u_1} {e : α} (M : Matroid α) (he : e ∉ M.E) : { N : Matroid α // e ∈ N.E ∧ N.delete {e} = M } ≃ M.ModularCut

Single-element extensions are equivalent to modular cuts.

Equations

• One or more equations did not get rendered due to their size.

theorem Matroid.ModularCut.mem_closure_extendBy_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) : e ∈ (M.extendBy e U).closure X ↔ e ∈ X ∨ M.closure X ∈ U

theorem Matroid.ModularCut.mem_closure_extendBy_dual_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (hXE : X ⊆ M.E := by aesop_mat) : e ∈ (M.extendBy e U)✶.closure X ↔ M.closure (M.E \ X) ∉ U

theorem Matroid.ModularCut.closure_mem_iff_mem_closure_extendBy {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (heX : e ∉ X) : M.closure X ∈ U ↔ e ∈ (M.extendBy e U).closure X

theorem Matroid.ModularCut.extendBy_closure_eq_self {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (heX : e ∉ X) (hXU : M.closure X ∉ U) : (M.extendBy e U).closure X = M.closure X

theorem Matroid.ModularCut.extendBy_closure_eq_insert {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (heX : e ∉ X) (hXSU : M.closure X ∈ U) : (M.extendBy e U).closure X = insert e (M.closure X)

theorem Matroid.ModularCut.extendBy_closure_insert_eq_insert {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (heX : e ∉ X) (hXSU : M.closure X ∈ U) : (M.extendBy e U).closure (insert e X) = insert e (M.closure X)

theorem Matroid.ModularCut.insert_isFlat_extendBy_of_mem {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (U : M.ModularCut) (hFU : F ∈ U) (he : e ∉ M.E) : (M.extendBy e U).IsFlat (insert e F)

theorem Matroid.ModularCut.isFlat_extendBy_of_isFlat_of_notMem {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (hF : M.IsFlat F) (hFU : F ∉ U) : (M.extendBy e U).IsFlat F

theorem Matroid.ModularCut.insert_isFlat_extendBy_of_not_covBy {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) (hF : M.IsFlat F) (h_not_covBy : ¬∃ F' ∈ U, F ⋖[M] F') : (M.extendBy e U).IsFlat (insert e F)

instance Matroid.ModularCut.instRankFiniteExtendBy {α : Type u_1} {M : Matroid α} (U : M.ModularCut) (e : α) [M.RankFinite] : (M.extendBy e U).RankFinite

An extension of a finite-rank matroid is finite.

theorem Matroid.ModularCut.extendBy_isColoop_iff {α : Type u_1} {M : Matroid α} {e : α} (U : M.ModularCut) (he : e ∉ M.E) : (M.extendBy e U).IsColoop e ↔ U = ⊥

theorem Matroid.ModularCut.extendBy_eRank_eq {α : Type u_1} {M : Matroid α} {e : α} (U : M.ModularCut) (hU : U ≠ ⊥) (he : e ∉ M.E) : (M.extendBy e U).eRank = M.eRank

@[simp]

theorem Matroid.ModularCut.extendBy_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} {U : M.ModularCut} : (M.extendBy e U).IsLoop e ↔ U = ⊤

@[simp]

theorem Matroid.ModularCut.extendBy_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {U : M.ModularCut} : (M.extendBy e U).IsNonloop e ↔ U ≠ ⊤

theorem Matroid.ModularCut.extendBy_isNonloop_dual_iff {α : Type u_1} {M : Matroid α} {e : α} {U : M.ModularCut} (he : e ∉ M.E) : (M.extendBy e U)✶.IsNonloop e ↔ U ≠ ⊥

theorem Matroid.ModularCut.extendBy_restrict_of_notMem {α : Type u_1} {M : Matroid α} {e : α} {U : M.ModularCut} {R : Set α} (he : e ∉ R) : (M.extendBy e U).restrict R = M.restrict R

theorem Matroid.ModularCut.extendBy_delete_of_mem {α : Type u_1} {M : Matroid α} {e : α} {U : M.ModularCut} {D : Set α} (he : e ∈ D) : (M.extendBy e U).delete D = M.delete D

theorem Matroid.ModularCut.mapEquiv_extendBy {α : Type u_1} {M : Matroid α} {e f : α} [DecidableEq α] (U : M.ModularCut) (he : e ∉ M.E) (hf : f ∉ M.E) : (M.extendBy e U).mapEquiv (Equiv.swap e f) = M.extendBy f U