@[simp]

theorem Matroid.ground_not_subset_loops {α : Type u_1} {M : Matroid α} [M.RankPos] : ¬M.E ⊆ M.loops

def Matroid.truncateToNat {α : Type u_1} (M : Matroid α) (k : ℕ) : Matroid α

The IndepMatroid whose independent sets are the M-independent sets of size at most k.

Equations

• M.truncateToNat k = (IndepMatroid.ofBddAugment M.E (fun (I : Set α) => M.Indep I ∧ I.encard ≤ ↑k) ⋯ ⋯ ⋯ ⋯ ⋯).matroid

def Matroid.truncateTo {α : Type u_1} (M : Matroid α) (k : ℕ∞) : Matroid α

The truncation of a matroid to rank k. The independent sets of the truncation are the independent sets of the matroid of size at most k.

Equations

• M.truncateTo k = Matroid.ofExistsMatroid M.E (fun (I : Set α) => M.Indep I ∧ I.encard ≤ k) ⋯

@[simp]

theorem Matroid.truncateTo_top {α : Type u_1} (M : Matroid α) : M.truncateTo ⊤ = M

@[simp]

theorem Matroid.truncateTo_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} {k : ℕ∞} : (M.truncateTo k).Indep I ↔ M.Indep I ∧ I.encard ≤ k

theorem Matroid.truncateTo_indep_eq {α : Type u_1} {M : Matroid α} {k : ℕ∞} : (M.truncateTo k).Indep = fun (I : Set α) => M.Indep I ∧ I.encard ≤ k

@[simp]

theorem Matroid.truncateTo_ground_eq {α : Type u_1} {M : Matroid α} {k : ℕ∞} : (M.truncateTo k).E = M.E

@[simp]

theorem Matroid.truncateTo_zero {α : Type u_1} (M : Matroid α) : M.truncateTo 0 = loopyOn M.E

@[simp]

theorem Matroid.truncateTo_emptyOn (α : Type u_2) (k : ℕ∞) : (emptyOn α).truncateTo k = emptyOn α

@[simp]

theorem Matroid.truncate_loopyOn {α : Type u_1} (E : Set α) (k : ℕ∞) : (loopyOn E).truncateTo k = loopyOn E

theorem Matroid.truncate_eq_self_of_rank_le {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h_rank : M.eRank ≤ k) : M.truncateTo k = M

theorem Matroid.truncateTo_isBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} {k : ℕ} (h_rank : ↑k ≤ M.eRank) : (M.truncateTo ↑k).IsBase B ↔ M.Indep B ∧ B.encard = ↑k

theorem Matroid.truncate_isBase_iff_of_rankFinite {α : Type u_1} {M : Matroid α} {B : Set α} {k : ℕ∞} [M.RankFinite] (h_rank : k ≤ M.eRank) : (M.truncateTo k).IsBase B ↔ M.Indep B ∧ B.encard = k

instance Matroid.truncateTo.finite {α : Type u_1} {M : Matroid α} {k : ℕ∞} [M.Finite] : (M.truncateTo k).Finite

instance Matroid.truncateTo.rankFinite {α : Type u_1} {M : Matroid α} {k : ℕ} : (M.truncateTo ↑k).RankFinite

theorem Matroid.Indep.of_truncateTo {α : Type u_1} {M : Matroid α} {I : Set α} {k : ℕ∞} (h : (M.truncateTo k).Indep I) : M.Indep I

theorem Matroid.Indep.encard_le_of_truncateTo {α : Type u_1} {M : Matroid α} {I : Set α} {k : ℕ∞} (h : (M.truncateTo k).Indep I) : I.encard ≤ k

theorem Matroid.truncateTo_eRk_eq {α : Type u_1} (M : Matroid α) (k : ℕ∞) (X : Set α) : (M.truncateTo k).eRk X = min (M.eRk X) k

theorem Matroid.truncate_aux {α : Type u_1} {M : Matroid α} {I : Set α} : (M.projectBy (ModularCut.principal M M.E)).Indep I ↔ M.Indep I ∧ (M.IsBase I → I = ∅)

def Matroid.truncate {α : Type u_1} (M : Matroid α) : Matroid α

The matroid on M.E whose independent sets are the independent nonbases of M.

Equations

• M.truncate = Matroid.ofExistsMatroid M.E (fun (I : Set α) => M.Indep I ∧ (M.IsBase I → I = ∅)) ⋯

@[simp]

theorem Matroid.truncate_ground_eq {α : Type u_1} {M : Matroid α} : M.truncate.E = M.E

theorem Matroid.truncate_indep_iff' {α : Type u_1} {M : Matroid α} {I : Set α} : M.truncate.Indep I ↔ M.Indep I ∧ (M.IsBase I → I = ∅)

@[simp]

theorem Matroid.truncate_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankPos] : M.truncate.Indep I ↔ M.Indep I ∧ ¬M.IsBase I

theorem Matroid.truncate_def {α : Type u_1} (M : Matroid α) : M.truncate = M.projectBy (ModularCut.principal M M.E)

theorem Matroid.Indep.of_truncate {α : Type u_1} {M : Matroid α} {I : Set α} (h : M.truncate.Indep I) : M.Indep I

theorem Matroid.truncate_dep_iff {α : Type u_1} {M : Matroid α} [M.RankPos] {D : Set α} : M.truncate.Dep D ↔ (M.Indep D → M.IsBase D) ∧ D ⊆ M.E

@[simp]

theorem Matroid.truncate_loopyOn_eq {α : Type u_1} {E : Set α} : (loopyOn E).truncate = loopyOn E

@[simp]

theorem Matroid.truncate_emptyOn_eq (α : Type u_2) : (emptyOn α).truncate = emptyOn α

instance Matroid.instNonemptyTruncate {α : Type u_1} {M : Matroid α} [M.Nonempty] : M.truncate.Nonempty

@[simp]

theorem Matroid.truncate_isBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankPos] : M.truncate.IsBase B ↔ ∃ e ∉ B, M.IsBase (insert e B)

theorem Matroid.IsBase.diff_singleton_truncate_isBase {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.IsBase B) (heB : e ∈ B) : M.truncate.IsBase (B \ {e})

theorem Matroid.Coindep.truncate_delete {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Coindep D) : (M.delete D).truncate = M.truncate.delete D

@[simp]

theorem Matroid.truncate_spanning_iff {α : Type u_1} {M : Matroid α} [M.RankPos] {S : Set α} : M.truncate.Spanning S ↔ ∃ e ∈ M.E, M.Spanning (insert e S)

theorem Matroid.truncate_spanning_iff_of_ssubset {α : Type u_1} {M : Matroid α} {S : Set α} (hssu : S ⊂ M.E) : M.truncate.Spanning S ↔ ∃ e ∈ M.E \ S, M.Spanning (insert e S)

theorem Matroid.Spanning.truncate_spanning {α : Type u_1} {M : Matroid α} {S : Set α} (hS : M.Spanning S) : M.truncate.Spanning S

theorem Matroid.IsHyperplane.truncate_spanning {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : M.truncate.Spanning H

theorem Matroid.truncate_restrict_of_not_spanning {α : Type u_1} {M : Matroid α} {R : Set α} (hSE : R ⊆ M.E) (hS : ¬M.Spanning R) : M.truncate.restrict R = M.restrict R

theorem Matroid.truncate_contract {α : Type u_1} (M : Matroid α) (C : Set α) : (M.contract C).truncate = M.truncate.contract C

instance Matroid.instRankPosDualTruncateOfNonempty {α : Type u_1} (M : Matroid α) [M.Nonempty] : M.truncate✶.RankPos

theorem Matroid.truncate_eRank_add_one {α : Type u_1} (M : Matroid α) [M.RankPos] : M.truncate.eRank + 1 = M.eRank

theorem Matroid.eRank_le_eRank_truncate_add_one {α : Type u_1} (M : Matroid α) : M.eRank ≤ M.truncate.eRank + 1

theorem Matroid.eRank_truncate_eq_eRank_sub_one {α : Type u_1} (M : Matroid α) : M.truncate.eRank = M.eRank - 1

@[simp]

theorem Matroid.truncate_spanning_iff_eRank_contract_le {α : Type u_1} {M : Matroid α} {S : Set α} (hSE : S ⊆ M.E := by aesop_mat) : M.truncate.Spanning S ↔ (M.contract S).eRank ≤ 1

@[simp]

theorem Matroid.truncate_rankPos_iff {α : Type u_1} {M : Matroid α} : M.truncate.RankPos ↔ 2 ≤ M.eRank

theorem Matroid.truncateTo_truncate {α : Type u_1} (M : Matroid α) (k : ℕ) (hk : ↑k + 1 ≤ M.eRank) : (M.truncateTo ↑(k + 1)).truncate = M.truncateTo ↑k

theorem Matroid.truncate_isCircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} [M.RankPos] : M.truncate.IsCircuit C ↔ M.IsCircuit C ∧ M.Nonspanning C ∨ M.IsBase C

theorem Matroid.truncate_isCircuit_iff' {α : Type u_1} {M : Matroid α} {C : Set α} : M.truncate.IsCircuit C ↔ M.IsCircuit C ∧ (M.Spanning C → C.Subsingleton) ∨ M.IsBase C ∧ C.Nonempty

A version of truncate_isCircuit_iff with no rankPos assumption

def Matroid.freeLift {α : Type u_1} (M : Matroid α) : Matroid α

Equations

• M.freeLift = M✶.truncate✶

@[simp]

theorem Matroid.freeLift_ground {α : Type u_1} (M : Matroid α) : M.freeLift.E = M.E

@[simp]

theorem Matroid.freeLift_freeOn {α : Type u_1} (E : Set α) : (freeOn E).freeLift = freeOn E

@[simp]

theorem Matroid.freeLift_emptyOn (α : Type u_2) : (emptyOn α).freeLift = emptyOn α

theorem Matroid.freeLift_isBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} [M✶.RankPos] : M.freeLift.IsBase B ↔ (∃ e ∈ B, M.IsBase (B \ {e})) ∧ B ⊆ M.E

@[simp]

theorem Matroid.freeLift_dual {α : Type u_1} (M : Matroid α) : M.freeLift✶ = M✶.truncate

@[simp]

theorem Matroid.truncate_dual {α : Type u_1} (M : Matroid α) : M.truncate✶ = M✶.freeLift

instance Matroid.instRankPosFreeLiftOfNonempty {α : Type u_1} {M : Matroid α} [M.Nonempty] : M.freeLift.RankPos

@[simp]

theorem Matroid.eRank_freeLift_eq {α : Type u_1} {M : Matroid α} [M✶.RankPos] : M.freeLift.eRank = M.eRank + 1

theorem Matroid.freeLift_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} : M.freeLift.Indep I ↔ I.Nonempty → ∃ e ∈ I ∩ M.E, M.Indep (I \ {e})

instance Matroid.instLooplessFreeLift {α : Type u_1} {M : Matroid α} : M.freeLift.Loopless

instance Matroid.instSimpleFreeLiftOfLoopless {α : Type u_1} {M : Matroid α} [M.Loopless] : M.freeLift.Simple

theorem Matroid.freeLift_dep_iff {α : Type u_1} {M : Matroid α} {D : Set α} : M.freeLift.Dep D ↔ D.Nonempty ∧ (∀ e ∈ D, M.Dep (D \ {e})) ∧ D ⊆ M.E

theorem Matroid.truncate_freeLift {α : Type u_1} (M : Matroid α) [M.RankPos] [M✶.RankPos] : M.truncate.freeLift = M.freeLift.truncate

theorem Matroid.freeLift_spanning_iff {α : Type u_1} {M : Matroid α} [M✶.RankPos] {X : Set α} : M.freeLift.Spanning X ↔ (∃ e ∈ X, M.Spanning (X \ {e})) ∧ X ⊆ M.E

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

The matroid on E whose ground set is a circuit. Empty if E = ∅.

Equations

• Matroid.circuitOn C = (Matroid.freeOn C).truncate

@[simp]

theorem Matroid.freeOn_truncate {α : Type u_1} (C : Set α) : (freeOn C).truncate = circuitOn C

@[simp]

theorem Matroid.circuitOn_ground {α : Type u_1} {C : Set α} : (circuitOn C).E = C

@[simp]

theorem Matroid.circuitOn_empty (α : Type u_2) : circuitOn ∅ = emptyOn α

theorem Matroid.circuitOn_indep_iff {α : Type u_1} {I C : Set α} (hC : C.Nonempty) : (circuitOn C).Indep I ↔ I ⊂ C

theorem Matroid.circuitOn_dep_iff {α : Type u_1} {C : Set α} (hC : C.Nonempty) {D : Set α} : (circuitOn C).Dep D ↔ D = C

theorem Matroid.circuitOn_isBase_iff {α : Type u_1} {B C : Set α} (hC : C.Nonempty) : (circuitOn C).IsBase B ↔ ∃ e ∉ B, insert e B = C

theorem Matroid.circuitOn_ground_isCircuit {α : Type u_1} {C : Set α} (hC : C.Nonempty) : (circuitOn C).IsCircuit C

theorem Matroid.circuitOn_isCircuit_iff {α : Type u_1} {C : Set α} (hC : C.Nonempty) {C' : Set α} : (circuitOn C).IsCircuit C' ↔ C' = C

theorem Matroid.circuitOn_spanning_iff {α : Type u_1} {C : Set α} (hC : C.Nonempty) {S : Set α} : (circuitOn C).Spanning S ↔ ∃ (e : α), insert e S = C

theorem Matroid.ground_isCircuit_iff {α : Type u_1} {M : Matroid α} [M.Nonempty] : M.IsCircuit M.E ↔ M = circuitOn M.E

theorem Matroid.eq_circuitOn_of_ground_isCircuit {α : Type u_1} {M : Matroid α} (h : M.IsCircuit M.E) : ∃ (E : Set α), E.Nonempty ∧ M = circuitOn E

theorem Matroid.isCircuit_iff_restr_eq_circuitOn {α : Type u_1} {M : Matroid α} {C : Set α} (hCne : C.Nonempty) (hC : C ⊆ M.E := by aesop_mat) : M.IsCircuit C ↔ M.restrict C = circuitOn C

theorem Matroid.IsCircuit.restrict_eq_circuitOn {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : M.restrict C = circuitOn C

@[simp]

theorem Matroid.circuitOn_freeLift {α : Type u_1} (C : Set α) : (circuitOn C).freeLift = freeOn C

@[simp]

theorem Matroid.circuitOn_singleton {α : Type u_1} (e : α) : circuitOn {e} = loopyOn {e}

@[simp]

theorem Matroid.circuitOn_contract {α : Type u_1} (C X : Set α) : (circuitOn C).contract X = circuitOn (C \ X)

theorem Matroid.circuitOn_delete {α : Type u_1} {C D : Set α} (hD : (C ∩ D).Nonempty) : (circuitOn C).delete D = freeOn (C \ D)

structure Matroid.TruncateFamily {α : Type u_1} (M : Matroid α) : Type u_1

A TruncateFamily is a collection of nonempty bases of M such that, for any two bases of M that both contain bases for a common hyperplane, either both or neither belongs to the collection. If M has finite rank or corank, the collection of all bases is the only TruncateFamily, but in general there can be others.

Given such a collection T, we can form a new matroid by making all the sets in T into spanning circuits instead of bases. In the special case where T contains all the bases of M, this operation is just truncation.

• ToTruncate : Set α → Prop
• forall_nonempty ⦃B : Set α⦄ : self.ToTruncate B → B.Nonempty
• forall_isBase ⦃B : Set α⦄ : self.ToTruncate B → M.IsBase B
• toTruncate_of_toTruncate ⦃B B' : Set α⦄ ⦃e e' : α⦄ : self.ToTruncate B → e ∈ B → M.IsBase B' → e' ∈ B' → M.closure (B \ {e}) = M.closure (B' \ {e'}) → self.ToTruncate B'

theorem Matroid.TruncateFamily.ext {α : Type u_1} {M : Matroid α} {x y : M.TruncateFamily} (ToTruncate : x.ToTruncate = y.ToTruncate) : x = y

theorem Matroid.TruncateFamily.ext_iff {α : Type u_1} {M : Matroid α} {x y : M.TruncateFamily} : x = y ↔ x.ToTruncate = y.ToTruncate

theorem Matroid.TruncateFamily.ToTruncate.isBase {α : Type u_1} {M : Matroid α} {B : Set α} {T : M.TruncateFamily} (hB : T.ToTruncate B) : M.IsBase B

theorem Matroid.TruncateFamily.ToTruncate.nonempty {α : Type u_1} {M : Matroid α} {B : Set α} {T : M.TruncateFamily} (hB : T.ToTruncate B) : B.Nonempty

theorem Matroid.TruncateFamily.ToTruncate.toTruncate_of_closure {α : Type u_1} {M : Matroid α} {I J : Set α} {e f : α} {T : M.TruncateFamily} (hI : T.ToTruncate (insert e I)) (heI : e ∉ I) (hfJ : f ∉ J) (hJ : M.Indep (insert f J)) (hIJ : I ⊆ M.closure J) : T.ToTruncate (insert f J)

theorem Matroid.TruncateFamily.ToTruncate.exchange {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} {T : M.TruncateFamily} (hB : T.ToTruncate B) (heB : e ∉ B) (hfB : f ∈ B) (h_indep : M.Indep (insert e (B \ {f}))) : T.ToTruncate (insert e (B \ {f}))

theorem Matroid.TruncateFamily.ToTruncate.of_exchange {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} {T : M.TruncateFamily} (hB' : T.ToTruncate (insert e (B \ {f}))) (heB : e ∉ B) (hfB : f ∈ B) (hB : M.IsBase B) : T.ToTruncate B

theorem Matroid.TruncateFamily.ToTruncate.finDiff {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} {B B' : Set α} (hB : T.ToTruncate B) (hB' : M.IsBase B') (hdiff : B.FinDiff B') : T.ToTruncate B'

def Matroid.TruncateFamily.Indep {α : Type u_1} {M : Matroid α} (T : M.TruncateFamily) (I : Set α) : Prop

Equations

• T.Indep I = (M.Indep I ∧ ¬T.ToTruncate I)

theorem Matroid.TruncateFamily.indep_eq {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} : T.Indep = fun (I : Set α) => M.Indep I ∧ ¬T.ToTruncate I

def Matroid.TruncateFamily.IsBase {α : Type u_1} {M : Matroid α} (T : M.TruncateFamily) (B : Set α) : Prop

Equations

• T.IsBase B = (M.IsBase B ∧ ¬T.ToTruncate B ∨ ∃ e ∈ M.E \ B, T.ToTruncate (insert e B))

theorem Matroid.TruncateFamily.isBase_eq {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} : T.IsBase = fun (B : Set α) => M.IsBase B ∧ ¬T.ToTruncate B ∨ ∃ e ∈ M.E \ B, T.ToTruncate (insert e B)

theorem Matroid.TruncateFamily.isBase_eq' {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} : T.IsBase = fun (B : Set α) => M.IsBase B ∧ ¬T.ToTruncate B ∨ ∃ e ∉ B, T.ToTruncate (insert e B)

theorem Matroid.TruncateFamily.ToTruncate.isBase_diff_singleton {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} {T : M.TruncateFamily} (hBt : T.ToTruncate B) (heB : e ∈ B) : T.IsBase (B \ {e})

theorem Matroid.TruncateFamily.ToTruncate.isBase_of_insert {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} {T : M.TruncateFamily} (hBt : T.ToTruncate (insert e B)) (heB : e ∉ B) : T.IsBase B

theorem Matroid.TruncateFamily.IsBase.indep {α : Type u_1} {M : Matroid α} {B : Set α} {T : M.TruncateFamily} (hB : T.IsBase B) : T.Indep B

theorem Matroid.TruncateFamily.IsBase.exists_toTruncate_insert {α : Type u_1} {M : Matroid α} {B : Set α} {T : M.TruncateFamily} (hB : T.IsBase B) (hBM : ¬M.IsBase B) : ∃ e ∈ M.E \ B, T.ToTruncate (insert e B)

theorem Matroid.TruncateFamily.Indep.indep {α : Type u_1} {M : Matroid α} {I : Set α} {T : M.TruncateFamily} (hI : T.Indep I) : M.Indep I

theorem Matroid.IsBase.partialTruncateBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} {T : M.TruncateFamily} (hB : M.IsBase B) : T.IsBase B ↔ ¬T.ToTruncate B

theorem Matroid.IsBase.partialTruncateBase {α : Type u_1} {M : Matroid α} {B : Set α} {T : M.TruncateFamily} (hB : M.IsBase B) (hBt : ¬T.ToTruncate B) : T.IsBase B

theorem Matroid.TruncateFamily.Indep.subset {α : Type u_1} {M : Matroid α} {I J : Set α} {T : M.TruncateFamily} (hI : T.Indep I) (hJI : J ⊆ I) : T.Indep J

theorem Matroid.TruncateFamily.maximal_indep_eq {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} : Maximal T.Indep = T.IsBase

def Matroid.TruncateFamily.matroid {α : Type u_1} {M : Matroid α} (T : M.TruncateFamily) : Matroid α

The Matroid formed by truncating all the bases in T.

Equations

• T.matroid = { E := M.E, Indep := T.Indep, indep_empty := ⋯, indep_subset := ⋯, indep_aug := ⋯, indep_maximal := ⋯, subset_ground := ⋯ }.matroid

@[simp]

theorem Matroid.TruncateFamily.matroid_E {α : Type u_1} {M : Matroid α} (T : M.TruncateFamily) : T.matroid.E = M.E

@[simp]

theorem Matroid.TruncateFamily.matroid_indep_eq {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} : T.matroid.Indep = T.Indep

@[simp]

theorem Matroid.TruncateFamily.matroid_isBase_eq {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} : T.matroid.IsBase = T.IsBase

theorem Matroid.TruncateFamily.matroid_closure_eq_closure {α : Type u_1} {M : Matroid α} {T : M.TruncateFamily} (X : Set α) (hX : X ⊆ M.E) : ¬T.matroid.Spanning X → T.matroid.closure X = M.closure X

def Matroid.TruncateFamily.top {α : Type u_1} (M : Matroid α) : M.TruncateFamily

The TruncateFamily consisting of all bases of M. This corresponds to the truncation of M. Empty if M has rank zero for technical reasons.

Equations

• Matroid.TruncateFamily.top M = { ToTruncate := fun (B : Set α) => M.IsBase B ∧ B.Nonempty, forall_nonempty := ⋯, forall_isBase := ⋯, toTruncate_of_toTruncate := ⋯ }

@[simp]

theorem Matroid.TruncateFamily.top_ToTruncate {α : Type u_1} (M : Matroid α) (B : Set α) : (top M).ToTruncate B = (M.IsBase B ∧ B.Nonempty)

@[simp]

theorem Matroid.TruncateFamily.matroid_top {α : Type u_1} {M : Matroid α} : (top M).matroid = M.truncate

def Matroid.TruncateFamily.bot {α : Type u_1} (M : Matroid α) : M.TruncateFamily

Equations

• Matroid.TruncateFamily.bot M = { ToTruncate := fun (B : Set α) => False, forall_nonempty := ⋯, forall_isBase := ⋯, toTruncate_of_toTruncate := ⋯ }

@[simp]

theorem Matroid.TruncateFamily.bot_ToTruncate {α : Type u_1} (M : Matroid α) (B : Set α) : (bot M).ToTruncate B = False

@[simp]

theorem Matroid.TruncateFamily.matroid_bot {α : Type u_1} {M : Matroid α} : (bot M).matroid = M

theorem Matroid.TruncateFamily.eq_top_or_bot_of_rankFinite {α : Type u_1} {M : Matroid α} [M.RankFinite] (T : M.TruncateFamily) : T = top M ∨ T = bot M

theorem Matroid.TruncateFamily.eq_top_or_bot_of_rankFinite_dual {α : Type u_1} {M : Matroid α} [M✶.RankFinite] (T : M.TruncateFamily) : T = top M ∨ T = bot M

theorem Matroid.truncate_closure_eq_of_not_spanning {α : Type u_1} {M : Matroid α} {X : Set α} (hXE : X ⊆ M.E := by aesop_mat) (hs : ¬M.truncate.Spanning X) : M.truncate.closure X = M.closure X

theorem Matroid.TruncateFamily.quotient {α : Type u_1} {M : Matroid α} (T : M.TruncateFamily) : T.matroid ≤q M

This gives an exotic example of a proper quotient that leaves some bases unchanged.

theorem Matroid.truncate_quotient {α : Type u_1} (M : Matroid α) : M.truncate ≤q M

theorem Matroid.Quotient.truncate {α : Type u_1} {M₁ M₂ : Matroid α} (h : M₂ ≤q M₁) : M₂.truncate ≤q M₁.truncate

theorem Matroid.project_quotient {α : Type u_1} (M : Matroid α) (X : Set α) : M.project X ≤q M

theorem Matroid.Quotient.project_quotient_project {α : Type u_1} {M₁ M₂ : Matroid α} (h : M₂ ≤q M₁) (X : Set α) : M₂.project X ≤q M₁.project X