def Matroid.«termB[_,_]» : Lean.ParserDescr

Equations

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

def Matroid.bDual {α : Type u_1} (M : Matroid α) (b : Bool) : Matroid α

Dualize M if b is true, otherwise don't. This is useful in self-dual settings.

Equations

• M.bDual b = bif b then M✶ else M

@[simp]

theorem Matroid.bDual_true {α : Type u_1} (M : Matroid α) : M.bDual true = M✶

@[simp]

theorem Matroid.bDual_false {α : Type u_1} (M : Matroid α) : M.bDual false = M

@[simp]

theorem Matroid.bDual_ground {α : Type u_1} (M : Matroid α) (b : Bool) : (M.bDual b).E = M.E

@[simp]

theorem Matroid.bDual_dual {α : Type u_1} (M : Matroid α) (b : Bool) : M✶.bDual b = M.bDual !b

@[simp]

theorem Matroid.dual_bDual {α : Type u_1} (M : Matroid α) (b : Bool) : (M.bDual b)✶ = M.bDual !b

theorem Matroid.bDual_not_dual {α : Type u_1} (M : Matroid α) (b : Bool) : (M✶.bDual !b) = M.bDual b

@[simp]

theorem Matroid.bDual_isCocircuit_iff {b : Bool} {α : Type u_1} {X : Set α} {M : Matroid α} : (M.bDual b).IsCocircuit X ↔ (M.bDual !b).IsCircuit X

theorem Matroid.bDual_coindep_iff {b : Bool} {α : Type u_1} {X : Set α} {M : Matroid α} : (M.bDual b).Coindep X ↔ (M.bDual !b).Indep X

theorem Matroid.bDual_map {b : Bool} {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) : (M.map f hf).bDual b = (M.bDual b).map f ⋯

@[simp]

theorem Matroid.bDual_bDual {b : Bool} {α : Type u_1} {M : Matroid α} {c : Bool} : (M.bDual b).bDual c = M.bDual (b != c)

theorem Matroid.bDual_bDual_self {α : Type u_1} (M : Matroid α) (b : Bool) : (M.bDual b).bDual b = M

theorem Matroid.eq_bDual_iff_bDual_eq {α : Type u_1} (M N : Matroid α) (d : Bool) : M.bDual d = N ↔ M = N.bDual d

theorem Matroid.bDual_isMinor_iff {α : Type u_1} {M : Matroid α} {d : Bool} {N : Matroid α} : N.bDual d ≤m M ↔ N ≤m M.bDual d

theorem Matroid.IsMinor.bDual {α : Type u_1} {M N : Matroid α} (hNM : N ≤m M) (b : Bool) : N.bDual b ≤m M.bDual b

theorem Matroid.IsStrictMinor.bDual {α : Type u_1} {M N : Matroid α} (hNM : N <m M) (b : Bool) : N.bDual b <m M.bDual b

instance Matroid.InvariantFun.bDual {γ₁ : Type u → Sort u_2} {γ₂ : Type u → Sort u_3} {δ₁ : Type v → Sort u_4} {δ₂ : Type v → Sort u_5} [Matroid.SupportClass γ₁] [Matroid.SupportClass γ₂] [Matroid.SupportClass δ₁] [Matroid.SupportClass δ₂] [Matroid.TransferClass γ₁ δ₁] [Matroid.TransferClass γ₂ δ₂] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] (b : Bool) : InvariantFun (fun {α : Type u} (M : Matroid α) (X : γ₁ α) => F (M.bDual b) X) fun {β : Type v} (N : Matroid β) (Y : δ₁ β) => G (N.bDual b) Y

def Matroid.remove {α : Type u_1} (M : Matroid α) (b : Bool) (X : Set α) : Matroid α

If b is false, then M ＼ X, and if b is true, then M ／ X. Used in self-dual settings.

Equations

• M.remove b X = bif b then M.contract X else M.delete X

@[simp]

theorem Matroid.remove_false {α : Type u_1} (M : Matroid α) (X : Set α) : M.remove false X = M.delete X

@[simp]

theorem Matroid.remove_true {α : Type u_1} (M : Matroid α) (X : Set α) : M.remove true X = M.contract X

@[simp]

theorem Matroid.remove_dual {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : (M.remove b X)✶ = M✶.remove (!b) X

theorem Matroid.dual_remove {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : M✶.remove b X = (M.remove (!b) X)✶

@[simp]

theorem Matroid.bDual_remove {α : Type u_1} (M : Matroid α) (X : Set α) (b c : Bool) : (M.remove c X).bDual b = (M.bDual b).remove (b != c) X

theorem Matroid.remove_bDual {α : Type u_1} (M : Matroid α) (X : Set α) (b c : Bool) : (M.bDual b).remove c X = (M.remove (b != c) X).bDual b

@[simp]

theorem Matroid.emptyOn_bDual (α : Type u_2) (b : Bool) : (emptyOn α).bDual b = emptyOn α

theorem Matroid.bDual_delete {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : (M.bDual b).delete X = (M.remove b X).bDual b

theorem Matroid.bDual_contract {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : (M.bDual b).contract X = (M.remove (!b) X).bDual b

theorem Matroid.delete_bDual {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : (M.delete X).bDual b = (M.bDual b).remove b X

theorem Matroid.contract_bDual {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : (M.contract X).bDual b = (M.bDual b).remove (!b) X

@[simp]

theorem Matroid.remove_ground {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : (M.remove b X).E = M.E \ X

@[simp]

theorem Matroid.remove_remove {α : Type u_1} (M : Matroid α) (X Y : Set α) (b : Bool) : (M.remove b X).remove b Y = M.remove b (X ∪ Y)

theorem Matroid.remove_comm {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : Disjoint X Y) (b c : Bool) : (M.remove b X).remove c Y = (M.remove c Y).remove b X

theorem Matroid.remove_isMinor {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : M.remove b X ≤m M

@[simp]

theorem Matroid.remove_inter_ground {α : Type u_1} (M : Matroid α) (X : Set α) (b : Bool) : M.remove b (X ∩ M.E) = M.remove b X

@[simp]

theorem Matroid.remove_singleton_eq_self {b : Bool} {α : Type u_1} {e : α} {M : Matroid α} : M.remove b {e} = M ↔ e ∉ M.E

theorem Matroid.remove_singleton_of_notMem {b : Bool} {α : Type u_1} {e : α} {M : Matroid α} (he : e ∉ M.E) : M.remove b {e} = M

theorem Matroid.IsStrictMinor.exists_isMinor_removeElem {α : Type u_1} {M N : Matroid α} (hNM : N <m M) : ∃ e ∈ M.E, ∃ (i : Bool), N ≤m M.remove i {e}

theorem Matroid.IsStrictMinor.exists_eq_remove_singleton {α : Type u_1} {M N : Matroid α} (hNM : N <m M) (hE : (M.E \ N.E).Subsingleton) : ∃ (b : Bool) (e : α), N = M.remove b {e}

theorem Matroid.IsMinor.exists_isMinor_removeElem {α : Type u_1} {e : α} {M N : Matroid α} (hNM : N ≤m M) (he : e ∉ N.E) : ∃ (b : Bool), N ≤m M.remove b {e}