@[simp]

theorem pair_subsingleton_iff {α : Type u_1} {x y : α} : {x, y}.Subsingleton ↔ x = y

def Matroid.unifOn {α : Type u_2} (E : Set α) (k : ℕ) : Matroid α

The uniform matroid with ground set E, whose independent sets are the finite sets of size at most k.

Equations

• Matroid.unifOn E k = (Matroid.freeOn E).truncateTo ↑k

@[simp]

theorem Matroid.unifOn_ground_eq {α : Type u_1} {k : ℕ} (E : Set α) : (unifOn E k).E = E

@[simp]

theorem Matroid.unifOn_indep_iff {α : Type u_1} {E I : Set α} {k : ℕ} : (unifOn E k).Indep I ↔ I.encard ≤ ↑k ∧ I ⊆ E

@[simp]

theorem Matroid.unifOn_zero {α : Type u_1} (E : Set α) : unifOn E 0 = loopyOn E

@[simp]

theorem Matroid.unifOn_empty (α : Type u_2) (a : ℕ) : unifOn ∅ a = emptyOn α

theorem Matroid.unifOn_truncate {α : Type u_1} (E : Set α) (k : ℕ) (hk : ↑k + 1 ≤ E.encard) : (unifOn E (k + 1)).truncate = unifOn E k

@[simp]

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

@[simp]

theorem Matroid.unifOn_freeLift {α : Type u_1} (E : Set α) (k : ℕ) : (unifOn E k).freeLift = unifOn E (k + 1)

theorem Matroid.unifOn_eq_of_le {α : Type u_1} {E : Set α} {k : ℕ} (h : E.encard ≤ ↑k) : unifOn E k = freeOn E

theorem Matroid.unifOn_pair {α : Type u_1} {e f : α} : unifOn {e, f} 2 = freeOn {e, f}

theorem Matroid.unifOn_pair_one {α : Type u_1} {e f : α} (hef : e ≠ f) : unifOn {e, f} 1 = circuitOn {e, f}

theorem Matroid.unifOn_triple {α : Type u_1} {e f g : α} : unifOn {e, f, g} 3 = freeOn {e, f, g}

theorem Matroid.unifOn_isBase_iff {α : Type u_1} {E B : Set α} {k : ℕ} (hk : ↑k ≤ E.encard) (hBE : B ⊆ E) : (unifOn E k).IsBase B ↔ B.encard = ↑k

theorem Matroid.unifOn_eRk_eq {α : Type u_1} {X : Set α} (E : Set α) (k : ℕ) (hX : X ⊆ E) : (unifOn E k).eRk X = min X.encard ↑k

theorem Matroid.unifOn_eRk_eq' {α : Type u_1} {X : Set α} (E : Set α) (k : ℕ) : (unifOn E k).eRk X = min (X ∩ E).encard ↑k

@[simp]

theorem Matroid.unifOn_eRank_eq {α : Type u_1} (E : Set α) (k : ℕ) : (unifOn E k).eRank = min E.encard ↑k

theorem Matroid.unifOn_eRank_eq' {α : Type u_1} {E : Set α} {k : ℕ} (hle : ↑k ≤ E.encard) : (unifOn E k).eRank = ↑k

theorem Matroid.unifOn_rank_eq {α : Type u_1} {E : Set α} {k : ℕ} (hk : ↑k ≤ E.encard) : (unifOn E k).rank = k

@[simp]

theorem Matroid.unifOn_rankPos_iff {α : Type u_1} {E : Set α} {k : ℕ} : (unifOn E k).RankPos ↔ 1 ≤ k ∧ E.Nonempty

instance Matroid.instRankFiniteUnifOn {α : Type u_1} {k : ℕ} {E : Set α} : (unifOn E k).RankFinite

theorem Matroid.unifOn_dual_eq {α : Type u_1} {E : Set α} {k : ℕ} (hE : E.Finite) : (unifOn E k)✶ = unifOn E (hE.toFinset.card - k)

theorem Matroid.unifOn_dual_eq' {α : Type u_1} {E : Set α} {j k : ℕ} (hE : E.encard = ↑k + ↑j) : (unifOn E k)✶ = unifOn E j

theorem Matroid.unifOn_dual_eq_of_le {α : Type u_1} {E : Set α} {k : ℕ} (hEfin : E.Finite) (hle : ↑k ≤ E.encard) : ∃ (j : ℕ), ↑j ≤ E.encard ∧ ↑k + ↑j = E.encard ∧ (unifOn E k)✶ = unifOn E j

theorem Matroid.unifOn_dual_eq_self {α : Type u_1} {k : ℕ} {E : Set α} (hkE : E.encard = 2 * ↑k) : (unifOn E k)✶ = unifOn E k

theorem Matroid.unifOn_bDual_eq_self {α : Type u_1} {k : ℕ} {E : Set α} (hkE : E.encard = 2 * ↑k) (d : Bool) : (unifOn E k).bDual d = unifOn E k

theorem Matroid.unifOn_spanning_iff' {α : Type u_1} {E X : Set α} {k : ℕ} : (unifOn E k).Spanning X ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E

theorem Matroid.unifOn_spanning_iff {α : Type u_1} {E X : Set α} {k : ℕ} (hk : ↑k ≤ E.encard) (hX : X ⊆ E) : (unifOn E k).Spanning X ↔ ↑k ≤ X.encard

theorem Matroid.unifOn_spanning_iff'' {α : Type u_1} {E X : Set α} {k : ℕ} (hk : ↑k ≤ E.encard) : (unifOn E k).Spanning X ↔ ↑k ≤ X.encard ∧ X ⊆ E

theorem Matroid.eq_unifOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} {k : ℕ} : M = unifOn E k ↔ M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ ↑k ∧ I ⊆ E

@[simp]

theorem Matroid.unifOn_delete_eq {α : Type u_1} (E D : Set α) (k : ℕ) : (unifOn E k).delete D = unifOn (E \ D) k

theorem Matroid.unifOn_contract_finset_eq {α : Type u_1} {E : Set α} {k : ℕ} {C : Finset α} (hCE : ↑C ⊆ E) : (unifOn E k).contract ↑C = unifOn (E \ ↑C) (k - C.card)

theorem Matroid.unifOn_contractElem {α : Type u_1} {E : Set α} {k : ℕ} {e : α} (heE : e ∈ E) : (unifOn E (k + 1)).contract {e} = unifOn (E \ {e}) k

theorem Matroid.unifOn_insert_contractElem {α : Type u_1} {E : Set α} {k : ℕ} {e : α} (he : e ∉ E) : (unifOn (insert e E) (k + 1)).contract {e} = unifOn E k

instance Matroid.unifOn_loopless {α : Type u_1} {k : ℕ} (E : Set α) : (unifOn E (k + 1)).Loopless

instance Matroid.unifOn_simple {α : Type u_1} {k : ℕ} (E : Set α) : (unifOn E (k + 2)).Simple

@[simp]

theorem Matroid.circuitOn_dual {α : Type u_1} (E : Set α) : (circuitOn E)✶ = unifOn E 1

@[simp]

theorem Matroid.unifOn_isCircuit_iff {α : Type u_1} {E C : Set α} {n : ℕ} : (unifOn E n).IsCircuit C ↔ C.encard = ↑n + 1 ∧ C ⊆ E

theorem Matroid.circuitOn_eq_unifOn {α : Type u_1} {C : Set α} {n : ℕ} (hn : ↑n + 1 = C.encard) : circuitOn C = unifOn C n

theorem Matroid.unifOn_coindep_iff' {α : Type u_1} {E I : Set α} {n : ℕ} (hIE : I ⊆ E) : (unifOn E n).Coindep I ↔ ↑n ≤ (E \ I).encard ∨ I = ∅

theorem Matroid.unifOn_coindep_iff {α : Type u_1} {E I : Set α} {n : ℕ} (hIE : I ⊆ E) (hnE : ↑n ≤ E.encard) : (unifOn E n).Coindep I ↔ ↑n ≤ (E \ I).encard

theorem Matroid.unifOn_coindep_iff'' {α : Type u_1} {E I : Set α} {n : ℕ} (hnE : ↑n ≤ E.encard) : (unifOn E n).Coindep I ↔ ↑n ≤ (E \ I).encard ∧ I ⊆ E

theorem Matroid.unifOn_isHyperplane_iff {α : Type u_1} {E : Set α} {n : ℕ} {H : Set α} (hnE : ↑n ≤ E.encard) : (unifOn E n).IsHyperplane H ↔ H.encard + 1 = ↑n ∧ H ⊆ E

theorem Matroid.unifOn_isCocircuit_iff {α : Type u_1} {E : Set α} {n : ℕ} {K : Set α} (hnE : ↑n ≤ E.encard) : (unifOn E n).IsCocircuit K ↔ (E \ K).encard + 1 = ↑n ∧ K ⊆ E

theorem Matroid.unifOn_loopless_iff {α : Type u_1} {E : Set α} {n : ℕ} : (unifOn E n).Loopless ↔ n = 0 → E = ∅

theorem Matroid.unifOn_coloopless_iff {α : Type u_1} {E : Set α} {n : ℕ} : (unifOn E n).Coloopless ↔ E.Nonempty → ↑n < E.encard

theorem Matroid.unifOn_simple_iff {α : Type u_1} {E : Set α} {n : ℕ} : (unifOn E n).Simple ↔ n = 0 ∧ E = ∅ ∨ n = 1 ∧ E.Subsingleton ∨ 2 ≤ n

@[simp]

theorem Matroid.unifOn_map {α : Type u_1} {β : Type u_2} (E : Set α) (f : α → β) (hf : Set.InjOn f E) (a : ℕ) : (unifOn E a).map f hf = unifOn (f '' E) a

def Matroid.unif (a b : ℕ) : Matroid (Fin b)

The canonical finite uniform matroid on ground type Fin b, whose independent sets are those of cardinality at most a.

Equations

• Matroid.unif a b = Matroid.unifOn Set.univ a

@[simp]

theorem Matroid.unif_ground_eq (a b : ℕ) : (unif a b).E = Set.univ

@[simp]

theorem Matroid.unif_indep_iff {a b : ℕ} (I : Set (Fin b)) : (unif a b).Indep I ↔ I.encard ≤ ↑a

@[simp]

theorem Matroid.unif_eRk_eq {a b : ℕ} (X : Set (Fin b)) : (unif a b).eRk X = min X.encard ↑a

@[simp]

theorem Matroid.unif_eRank_eq (a b : ℕ) : (unif a b).eRank = ↑(min a b)

@[simp]

theorem Matroid.unif_rank_eq (a b : ℕ) : (unif a b).rank = min a b

theorem Matroid.unif_eRank_eq_of_le {a b : ℕ} (hab : a ≤ b) : (unif a b).eRank = ↑a

theorem Matroid.unif_isBase_iff {a b : ℕ} (hab : a ≤ b) {B : Set (Fin b)} : (unif a b).IsBase B ↔ B.encard = ↑a

@[simp]

theorem Matroid.unif_isBase_iff' {a b : ℕ} {B : Set (Fin (a + b))} : (unif a (a + b)).IsBase B ↔ B.encard = ↑a

@[simp]

theorem Matroid.unif_isCircuit_iff {a b : ℕ} {C : Set (Fin b)} : (unif a b).IsCircuit C ↔ C.encard = ↑a + 1

theorem Matroid.unif_dual' {a b n : ℕ} (h : a + b = n) : (unif a n)✶ = unif b n

@[simp]

theorem Matroid.unif_add_left_dual (a b : ℕ) : (unif a (a + b))✶ = unif b (a + b)

@[simp]

theorem Matroid.unif_add_right_dual (a b : ℕ) : (unif b (a + b))✶ = unif a (a + b)

instance Matroid.unif_loopless (a b : ℕ) : (unif (a + 1) b).Loopless

instance Matroid.unif_simple (a b : ℕ) : (unif (a + 2) b).Simple

@[simp]

theorem Matroid.unif_zero (b : ℕ) : unif 0 b = loopyOn Set.univ

theorem Matroid.unif_eq_freeOn {a b : ℕ} (h : b ≤ a) : unif a b = freeOn Set.univ

theorem Matroid.unif_eq_unif_min {a b : ℕ} : unif a b = unif (min a b) b

theorem Matroid.unif_dual (a b : ℕ) : (unif a b)✶ = unif (b - a) b

The expression for dual of a uniform matroid. The junk case where b < a still works because the subtraction truncates.

theorem Matroid.unif_sub_dual (a b : ℕ) : (unif (b - a) b)✶ = unif a b

@[simp]

theorem Matroid.unif_self_dual (a : ℕ) : (unif a (2 * a))✶ = unif a (2 * a)

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

Uniformity as a predicate ; a matroid is uniform if every subset of the ground set is independent or spanning. This is mainly useful for infinite matroids, where uniformity is structurally nontrivial.

Equations

• M.IsUniform = ∀ ⦃X : Set α⦄, X ⊆ M.E → M.Indep X ∨ M.Spanning X

theorem Matroid.IsUniform.indep_or_spanning {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : M.Indep X ∨ M.Spanning X

theorem Matroid.isUniform_iff {α : Type u_1} {M : Matroid α} : M.IsUniform ↔ ∀ ⦃X : Set α⦄, X ⊆ M.E → M.Indep X ∨ M.Spanning X

theorem Matroid.IsUniform.indep_of_nonspanning {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M.IsUniform) (h : M.Nonspanning X) : M.Indep X

theorem Matroid.IsUniform.spanning_of_dep {α : Type u_1} {M : Matroid α} {X : Set α} (hM : M.IsUniform) (h : M.Dep X) : M.Spanning X

theorem Matroid.IsUniform.inter_nonempty_of_dep_codep {α : Type u_1} {M : Matroid α} {X Y : Set α} (hM : M.IsUniform) (hX : M.Dep X) (hcd : M.Codep Y) : (X ∩ Y).Nonempty

theorem Matroid.isUniform_iff_circuit_cocircuit {α : Type u_1} {M : Matroid α} : M.IsUniform ↔ ∀ ⦃C K : Set α⦄, M.IsCircuit C → M.IsCocircuit K → (C ∩ K).Nonempty

A matroid is uniform iff every circuit intersects every cocircuit.

theorem Matroid.isUniform_iff_forall_spanning_of_isCircuit {α : Type u_1} {M : Matroid α} : M.IsUniform ↔ ∀ (C : Set α), M.IsCircuit C → M.Spanning C

theorem Matroid.IsUniform.dual {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) : M✶.IsUniform

theorem Matroid.IsUniform.not_isCircuitHyperplane {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) (C : Set α) : ¬M.IsCircuitHyperplane C

@[simp]

theorem Matroid.uniform_dual_iff {α : Type u_1} {M : Matroid α} : M✶.IsUniform ↔ M.IsUniform

theorem Matroid.isUniform_iff_forall_isFreeBase {α : Type u_1} {M : Matroid α} : M.IsUniform ↔ ∀ (B : Set α), M.IsBase B → M.IsFreeBase B

theorem Matroid.IsUniform.isFreeBase {α : Type u_1} {M : Matroid α} {B : Set α} (hM : M.IsUniform) (hB : M.IsBase B) : M.IsFreeBase B

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

theorem Matroid.IsUniform.isBase_of_isBase_of_finDiff {α : Type u_1} {M : Matroid α} {B B' : Set α} (hM : M.IsUniform) (hB : M.IsBase B) (h_fin : B.FinDiff B') (hB' : B' ⊆ M.E) : M.IsBase B'

theorem Matroid.IsUniform.insert_isCircuit_of_isBase {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hM : M.IsUniform) (hB : M.IsBase B) (he : e ∈ M.E \ B) : M.IsCircuit (insert e B)

theorem Matroid.uniform_iff_forall_insert_diff_singleton {α : Type u_1} {M : Matroid α} : M.IsUniform ↔ ∀ ⦃B : Set α⦄ ⦃e f : α⦄, M.IsBase B → e ∈ M.E \ B → f ∈ B → M.IsBase (insert e (B \ {f}))

theorem Matroid.IsUniform.contract {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) (C : Set α) : (M.contract C).IsUniform

theorem Matroid.IsUniform.delete {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) (D : Set α) : (M.delete D).IsUniform

theorem Matroid.IsUniform.minor {α : Type u_1} {M N : Matroid α} (hM : M.IsUniform) (hNM : N ≤m M) : N.IsUniform

@[simp]

theorem Matroid.loopyOn_uniform {α : Type u_1} (E : Set α) : (loopyOn E).IsUniform

@[simp]

theorem Matroid.freeOn_uniform {α : Type u_1} (E : Set α) : (freeOn E).IsUniform

theorem Matroid.IsUniform.truncate {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) : M.truncate.IsUniform

@[simp]

theorem Matroid.isUniform_unifOn {α : Type u_1} (E : Set α) (a : ℕ) : (unifOn E a).IsUniform

theorem Matroid.IsUniform.closure_not_spanning {α : Type u_1} {M : Matroid α} {I : Set α} (hM : M.IsUniform) (hIE : I ⊆ M.E) (hIs : ¬M.Spanning I) : M.closure I = I

theorem Matroid.IsUniform.of_iso {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) {β : Type u_2} {N : Matroid β} (e : M ≂ N) : N.IsUniform

theorem Matroid.Iso.isUniform_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {N : Matroid β} (e : M ≂ N) : M.IsUniform ↔ N.IsUniform

theorem Matroid.IsUniform.map {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) : (M.map f hf).IsUniform

theorem Matroid.maximal_right_of_forall_ge {α : Type u_2} {P Q : α → Prop} {a : α} [PartialOrder α] (hP : ∀ ⦃x y : α⦄, P x → x ≤ y → P y) (h : Maximal (fun (x : α) => P x ∧ Q x) a) : Maximal Q a

def Matroid.uniformMatroidOfBase {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (Set.ofPred IsBase)) (exchange : ∀ ⦃B : Set α⦄ ⦃e f : α⦄, IsBase B → e ∈ B → f ∈ E \ B → IsBase (insert f (B \ {e}))) (contain : ∀ ⦃I X : Set α⦄, I ⊆ X → X ⊆ E → (X \ I).Infinite → ∃ (B : Set α), IsBase B ∧ (B ⊆ I ∨ I ⊆ B ∧ B ⊆ X ∨ X ⊆ B)) (subset_ground : ∀ ⦃B : Set α⦄, IsBase B → B ⊆ E) : Matroid α

Equations

• Matroid.uniformMatroidOfBase E IsBase exists_isBase antichain exchange contain subset_ground = Matroid.ofBase E IsBase exists_isBase ⋯ ⋯ subset_ground

@[simp]

theorem Matroid.uniformMatroidOfBase_Indep {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (Set.ofPred IsBase)) (exchange : ∀ ⦃B : Set α⦄ ⦃e f : α⦄, IsBase B → e ∈ B → f ∈ E \ B → IsBase (insert f (B \ {e}))) (contain : ∀ ⦃I X : Set α⦄, I ⊆ X → X ⊆ E → (X \ I).Infinite → ∃ (B : Set α), IsBase B ∧ (B ⊆ I ∨ I ⊆ B ∧ B ⊆ X ∨ X ⊆ B)) (subset_ground : ∀ ⦃B : Set α⦄, IsBase B → B ⊆ E) (I : Set α) : (uniformMatroidOfBase E IsBase exists_isBase antichain exchange contain subset_ground).Indep I = ∃ (B : Set α), IsBase B ∧ I ⊆ B

@[simp]

theorem Matroid.uniformMatroidOfBase_IsBase {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (Set.ofPred IsBase)) (exchange : ∀ ⦃B : Set α⦄ ⦃e f : α⦄, IsBase B → e ∈ B → f ∈ E \ B → IsBase (insert f (B \ {e}))) (contain : ∀ ⦃I X : Set α⦄, I ⊆ X → X ⊆ E → (X \ I).Infinite → ∃ (B : Set α), IsBase B ∧ (B ⊆ I ∨ I ⊆ B ∧ B ⊆ X ∨ X ⊆ B)) (subset_ground : ∀ ⦃B : Set α⦄, IsBase B → B ⊆ E) (a✝ : Set α) : (uniformMatroidOfBase E IsBase exists_isBase antichain exchange contain subset_ground).IsBase a✝ = IsBase a✝

@[simp]

theorem Matroid.uniformMatroidOfBase_E {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ (B : Set α), IsBase B) (antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (Set.ofPred IsBase)) (exchange : ∀ ⦃B : Set α⦄ ⦃e f : α⦄, IsBase B → e ∈ B → f ∈ E \ B → IsBase (insert f (B \ {e}))) (contain : ∀ ⦃I X : Set α⦄, I ⊆ X → X ⊆ E → (X \ I).Infinite → ∃ (B : Set α), IsBase B ∧ (B ⊆ I ∨ I ⊆ B ∧ B ⊆ X ∨ X ⊆ B)) (subset_ground : ∀ ⦃B : Set α⦄, IsBase B → B ⊆ E) : (uniformMatroidOfBase E IsBase exists_isBase antichain exchange contain subset_ground).E = E

theorem Matroid.uniformMatroidOfBase_uniform {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) {exists_isBase : ∃ (B : Set α), IsBase B} {ac : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (Set.ofPred IsBase)} {exch : ∀ ⦃B : Set α⦄ ⦃e f : α⦄, IsBase B → e ∈ B → f ∈ E \ B → IsBase (insert f (B \ {e}))} {contain : ∀ ⦃I X : Set α⦄, I ⊆ X → X ⊆ E → (X \ I).Infinite → ∃ (B : Set α), IsBase B ∧ (B ⊆ I ∨ I ⊆ B ∧ B ⊆ X ∨ X ⊆ B)} {subset_ground : ∀ ⦃B : Set α⦄, IsBase B → B ⊆ E} : (uniformMatroidOfBase E IsBase exists_isBase ac exch contain subset_ground).IsUniform