structure Matroid.IsFreeBase {α : Type u_1} (M : Matroid α) (B : Set α) : Prop

A free base is one where exchanging any two elements gives a base.

• isBase : M.IsBase B
• isBase_of_exchange (B' : Set α) : B' ⊆ M.E → B'.IsExchange B → M.IsBase B'

theorem Matroid.isFreeBase_iff {α : Type u_1} (M : Matroid α) (B : Set α) : M.IsFreeBase B ↔ M.IsBase B ∧ ∀ B' ⊆ M.E, B'.IsExchange B → M.IsBase B'

theorem Matroid.IsFreeBase.subset_ground {α : Type u_1} {M : Matroid α} {B : Set α} (h : M.IsFreeBase B) : B ⊆ M.E

theorem Matroid.IsFreeBase.isBase_insert_diff_singleton {α : Type u_1} {M : Matroid α} {e f : α} {B : Set α} (h : M.IsFreeBase B) (he : e ∈ B) (hf : f ∈ M.E \ B) : M.IsBase (insert f (B \ {e}))

theorem Matroid.IsFreeBase.compl_dual {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsFreeBase B) : M✶.IsFreeBase (M.E \ B)

theorem Matroid.isFreeBase_dual_iff {α : Type u_1} {M : Matroid α} {B : Set α} (hB : B ⊆ M.E) : M✶.IsFreeBase B ↔ M.IsFreeBase (M.E \ B)

theorem Matroid.IsFreeBase.indep_of_ssubset_insert {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {B : Set α} (hB : M.IsFreeBase B) (hI : I ⊂ insert e B) (he : e ∈ M.E := by aesop_mat) : M.Indep I

instance Matroid.instGroundedPredSetIsFreeBase : GroundedPred fun {α : Type u_2} => IsFreeBase

instance Matroid.instInvariantFunSetPropIsFreeBase : InvariantFun (fun {α : Type u_2} => IsFreeBase) fun {β : Type u_3} => IsFreeBase

theorem Matroid.IsBase.isBase_of_indep_of_finDiff {α : Type u_1} {M : Matroid α} {I B : Set α} (hB : M.IsBase B) (hI : M.Indep I) (hBI : B.FinDiff I) : M.IsBase I

theorem Matroid.IsBase.isBase_of_spanning_of_finDiff {α : Type u_1} {M : Matroid α} {B S : Set α} (hB : M.IsBase B) (hS : M.Spanning S) (hBS : B.FinDiff S) : M.IsBase S

theorem Matroid.IsBase.eq_of_isBase_finDiff_finDiff_subset {α : Type u_1} {M : Matroid α} {B C X Y : Set α} (hB : M.IsBase B) (hBX : B.FinDiff X) (hC : M.IsBase C) (hCY : C.FinDiff Y) (hXY : X ⊆ Y) : X = Y

theorem Matroid.isAntichain_setOf_finDiff_isBase {α : Type u_1} (M : Matroid α) : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) {X : Set α | ∃ (B : Set α), M.IsBase B ∧ B.FinDiff X}

The collection of sets that are FinDiff of some base is an antichain. (for a finite-rank matroid M, these are the sets whos cardinality is the rank of M.)

theorem Matroid.IsBase.finDiff_iff_encard_eq_eRank {α : Type u_1} {M : Matroid α} {B X : Set α} [M.RankFinite] (hB : M.IsBase B) : B.FinDiff X ↔ X.encard = M.eRank

theorem Matroid.IsCircuitHyperplane.insert_diff_singleton_isBase {α : Type u_1} {M : Matroid α} {H : Set α} {e f : α} (hH : M.IsCircuitHyperplane H) (he : e ∈ H) (hf : f ∈ M.E \ H) : M.IsBase (insert f (H \ {e}))

theorem Matroid.IsCircuit.isHyperplane_of_forall_isBase_of_isExchange {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (hex : ∀ B ⊆ M.E, B.IsExchange C → M.IsBase B) (hCE : C ⊂ M.E) : M.IsHyperplane C

theorem Matroid.IsCircuitHyperplane.isBase_of_isExchange {α : Type u_1} {M : Matroid α} {B H : Set α} (hH : M.IsCircuitHyperplane H) (hB : B ⊆ M.E) (hHB : H.IsExchange B) : M.IsBase B

structure Matroid.IsNonbase {α : Type u_1} (M : Matroid α) (K : Set α) : Prop

M.IsNonbase K means that K is not a base, but differs from a base by a finite number of exchanges. For a matroid of rank r ≠ ∞, this amounts to saying that K is a dependent r-set.

• subset_ground : K ⊆ M.E
• not_isBase : ¬M.IsBase K
• exists_findiff : ∃ (B : Set α), M.IsBase B ∧ B.FinDiff K

theorem Matroid.isNonbase_iff {α : Type u_1} (M : Matroid α) (K : Set α) : M.IsNonbase K ↔ K ⊆ M.E ∧ ¬M.IsBase K ∧ ∃ (B : Set α), M.IsBase B ∧ B.FinDiff K

instance Matroid.instGroundedPredSetIsNonbase : GroundedPred fun {α : Type u_2} => IsNonbase

instance Matroid.instInvariantFunSetPropIsNonbase : InvariantFun (fun {α : Type u_2} => IsNonbase) fun {β : Type u_3} => IsNonbase

theorem Matroid.IsNonbase.compl_isNonbase_dual {α : Type u_1} {M : Matroid α} {K : Set α} (h : M.IsNonbase K) : M✶.IsNonbase (M.E \ K)

theorem Matroid.isNonbase_dual_iff {α : Type u_1} {M : Matroid α} {K : Set α} (hK : K ⊆ M.E := by aesop_mat) : M✶.IsNonbase K ↔ M.IsNonbase (M.E \ K)

theorem Matroid.IsNonbase.dep {α : Type u_1} {M : Matroid α} {K : Set α} (h : M.IsNonbase K) : M.Dep K

theorem Matroid.IsNonbase.nonspanning {α : Type u_1} {M : Matroid α} {K : Set α} (h : M.IsNonbase K) : M.Nonspanning K

theorem Matroid.isNonbase_iff_encard {α : Type u_1} {M : Matroid α} {K : Set α} [M.RankFinite] (hKE : K ⊆ M.E) : M.IsNonbase K ↔ K.encard = M.eRank ∧ ¬M.IsBase K

theorem Matroid.isNonbase_iff_not_isBase {α : Type u_1} {M : Matroid α} {K : Set α} [M.RankFinite] (hKE : K ⊆ M.E) (hKcard : K.encard = M.eRank) : M.IsNonbase K ↔ ¬M.IsBase K