structure Matroid.IsFiniteRankUniform {α : Type u_1} (M : Matroid α) (a : ℕ) : Prop

M.IsFiniteRankUniform a means that M is a uniform matroid of rank a ∈ ℕ.

• eRank_eq : M.eRank = ↑a
• isUniform : M.IsUniform

theorem Matroid.isFiniteRankUniform_iff {α : Type u_1} (M : Matroid α) (a : ℕ) : M.IsFiniteRankUniform a ↔ M.eRank = ↑a ∧ M.IsUniform

theorem Matroid.IsFiniteRankUniform.le {α : Type u_1} {M : Matroid α} {a : ℕ} (h : M.IsFiniteRankUniform a) : ↑a ≤ M.E.encard

theorem Matroid.IsFiniteRankUniform.rankFinite {α : Type u_1} {M : Matroid α} {a : ℕ} (h : M.IsFiniteRankUniform a) : M.RankFinite

theorem Matroid.IsFiniteRankUniform.eq_unifOn {α : Type u_1} {M : Matroid α} {a : ℕ} (h : M.IsFiniteRankUniform a) : M = unifOn M.E a

theorem Matroid.IsFiniteRankUniform.exists_eq_unifOn {α : Type u_1} {M : Matroid α} {a : ℕ} (h : M.IsFiniteRankUniform a) : ∃ (E : Set α), M = unifOn E a ∧ ↑a ≤ E.encard

theorem Matroid.unifOn_isFiniteRankUniform {α : Type u_1} {E : Set α} {a : ℕ} (haE : ↑a ≤ E.encard) : (unifOn E a).IsFiniteRankUniform a

theorem Matroid.isFiniteRankUniform_iff_eq_unifOn {α : Type u_1} {M : Matroid α} {a : ℕ} : M.IsFiniteRankUniform a ↔ M = unifOn M.E a ∧ ↑a ≤ M.E.encard

theorem Matroid.IsFiniteRankUniform.indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.Indep I ↔ I.encard ≤ ↑a ∧ I ⊆ M.E

theorem Matroid.isFiniteRankUniform_iff_forall_indep_iff {α : Type u_1} {M : Matroid α} {a : ℕ} : M.IsFiniteRankUniform a ↔ ↑a ≤ M.E.encard ∧ ∀ I ⊆ M.E, M.Indep I ↔ I.encard ≤ ↑a

theorem Matroid.IsFiniteRankUniform.isCircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.IsCircuit C ↔ C.encard = ↑a + 1 ∧ C ⊆ M.E

theorem Matroid.IsFiniteRankUniform.dep_iff {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.Dep X ↔ ↑a < X.encard ∧ X ⊆ M.E

theorem Matroid.IsFiniteRankUniform.isBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.IsBase B ↔ B.encard = ↑a ∧ B ⊆ M.E

theorem Matroid.IsFiniteRankUniform.isCocircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.IsCocircuit C ↔ (M.E \ C).encard + 1 = ↑a ∧ C ⊆ M.E

theorem Matroid.IsFiniteRankUniform.spanning_iff {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.Spanning X ↔ ↑a ≤ X.encard ∧ X ⊆ M.E

theorem Matroid.IsFiniteRankUniform.restrict {α : Type u_1} {M : Matroid α} {a : ℕ} (hM : M.IsFiniteRankUniform a) {R : Set α} (hRX : R ⊆ M.E) (haR : ↑a ≤ R.encard) : (M.restrict R).IsFiniteRankUniform a

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

theorem Matroid.IsFiniteRankUniform.loopless_iff {α : Type u_1} {M : Matroid α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.Loopless ↔ a = 0 → M = emptyOn α

theorem Matroid.IsFiniteRankUniform.simple_iff {α : Type u_1} {M : Matroid α} {a : ℕ} (hM : M.IsFiniteRankUniform a) : M.Simple ↔ a ≤ 1 → M.E.encard ≤ ↑a

theorem Matroid.IsUniform.isFiniteRankUniform {α : Type u_1} {M : Matroid α} [M.RankFinite] (hM : M.IsUniform) : ∃ (a : ℕ), M.IsFiniteRankUniform a

A uniform matroid whose rank is finite is one of the obvious ones.

theorem Matroid.IsUniform.isFiniteRankUniform_of_finitary {α : Type u_1} {M : Matroid α} [M.Finitary] [M✶.RankPos] (hM : M.IsUniform) : ∃ (a : ℕ), M.IsFiniteRankUniform a

A finitary non-free uniform matroid is a finite-rank uniform matroid.

theorem Matroid.IsUniform.eq_freeOn_or_isFiniteRankUniform {α : Type u_1} {M : Matroid α} [M.Finitary] (hM : M.IsUniform) : ∃ (E : Set α), M = freeOn E ∨ ∃ (a : ℕ), M.IsFiniteRankUniform a

@[simp]

theorem Matroid.isFiniteRankUniform_zero_iff {α : Type u_1} {M : Matroid α} : M.IsFiniteRankUniform 0 ↔ M.eRank = 0

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

theorem Matroid.Iso.isFiniteRankUniform_iff {α : Type u_1} {M : Matroid α} {a : ℕ} {β : Type u_2} {N : Matroid β} (e : M ≂ N) : M.IsFiniteRankUniform a ↔ N.IsFiniteRankUniform a

theorem Matroid.nonempty_iso_unifOn_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {X : Set β} {a : ℕ} (haX : ↑a ≤ X.encard) : Nonempty (M ≂ unifOn X a) ↔ M.IsFiniteRankUniform a ∧ Nonempty (↑X ≃ ↑M.E)

structure Matroid.IsFiniteRankUniformOn {α : Type u_1} (M : Matroid α) (a : ℕ) (X : Set α) : Prop

The restriction of M to X is a rank-a uniform matroid

• isFiniteRankUniform : (M.restrict X).IsFiniteRankUniform a
• subset_ground : X ⊆ M.E

theorem Matroid.isFiniteRankUniformOn_iff {α : Type u_1} (M : Matroid α) (a : ℕ) (X : Set α) : M.IsFiniteRankUniformOn a X ↔ (M.restrict X).IsFiniteRankUniform a ∧ X ⊆ M.E

theorem Matroid.IsFiniteRankUniformOn.eRk {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} (h : M.IsFiniteRankUniformOn a X) : M.eRk X = ↑a

theorem Matroid.IsFiniteRankUniform.isFiniteRankUniformOn_of_restrict' {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} (h : (M.restrict X).IsFiniteRankUniform a) (ha : a ≠ 0) : M.IsFiniteRankUniformOn a X

@[simp]

theorem Matroid.isFiniteRankUniformOn_zero_iff {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsFiniteRankUniformOn 0 X ↔ X ⊆ M.loops

theorem Matroid.IsFiniteRankUniform.isFiniteRankUniformOn_of_restrict {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} (h : (M.restrict X).IsFiniteRankUniform a) (hXE : X ⊆ M.E := by aesop_mat) : M.IsFiniteRankUniformOn a X

theorem Matroid.isFiniteRankUniformOn_iff_indep {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} (ha : a ≠ 0) : M.IsFiniteRankUniformOn a X ↔ ↑a ≤ X.encard ∧ ∀ I ⊆ X, M.Indep I ↔ I.encard ≤ ↑a

theorem Matroid.IsFiniteRankUniformOn.subset {α : Type u_1} {M : Matroid α} {X Y : Set α} {a : ℕ} (h : M.IsFiniteRankUniformOn a X) (hYX : Y ⊆ X) (hY : ↑a ≤ Y.encard) : M.IsFiniteRankUniformOn a Y

theorem Matroid.isFiniteRankUniform_restrict_iff {α : Type u_1} {M : Matroid α} {X : Set α} {a : ℕ} : (M.restrict X).IsFiniteRankUniform a ↔ ↑a ≤ X.encard ∧ ∀ I ⊆ X, M.Indep I ↔ I.encard ≤ ↑a

theorem Matroid.IsFiniteRankUniform.restrict_insert_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} {a : ℕ} (h : (M.restrict X).IsFiniteRankUniform (a + 1)) (heX : e ∉ X) (he : e ∈ M.closure X) : (M.restrict (insert e X)).IsFiniteRankUniform (a + 1) ↔ ∀ I ⊆ X, I.encard = ↑a → e ∉ M.closure I

theorem Matroid.IsFiniteRankUniform.contract {α : Type u_1} {M : Matroid α} {C : Set α} {a b : ℕ} (h : M.IsFiniteRankUniform a) (hC : C ⊆ M.E) (hab : ↑a = ↑b + C.encard) : (M.contract C).IsFiniteRankUniform b

theorem Matroid.IsFiniteRankUniform.contractElem {α : Type u_1} {M : Matroid α} {e : α} {a : ℕ} (h : M.IsFiniteRankUniform (a + 1)) (he : e ∈ M.E) : (M.contract {e}).IsFiniteRankUniform a

structure Matroid.IsFiniteUniform {α : Type u_1} (M : Matroid α) (a b : ℕ) (n : ℕ := a + b) extends M.IsFiniteRankUniform a : Prop

M.IsFiniteUniform a b n means that M is a finite uniform matroid of rank a and corank b, with n elements.

We have a + b = n for every such matroid, but the redundancy helps with duality.

• eRank_eq : M.eRank = ↑a
• isUniform : M.IsUniform
• encard_eq : M.E.encard = ↑n
• eRank_dual_eq : M✶.eRank = ↑b

theorem Matroid.isFiniteUniform_iff {α : Type u_1} (M : Matroid α) (a b : ℕ) (n : ℕ := a + b) : M.IsFiniteUniform a b n ↔ M.IsFiniteRankUniform a ∧ M.E.encard = ↑n ∧ M✶.eRank = ↑b

theorem Matroid.isFiniteUniform_iff' {α : Type u_1} {M : Matroid α} {a b : ℕ} : M.IsFiniteUniform a b ↔ M.IsFiniteRankUniform a ∧ M.E.encard = ↑a + ↑b

theorem Matroid.isFiniteUniform_iff_dual {α : Type u_1} {M : Matroid α} {a b : ℕ} : M.IsFiniteUniform a b ↔ M.IsFiniteRankUniform a ∧ M✶.IsFiniteRankUniform b

theorem Matroid.IsFiniteUniform.finite {α : Type u_1} {M : Matroid α} {a b n : ℕ} (hM : M.IsFiniteUniform a b n) : M.Finite

theorem Matroid.IsFiniteUniform.add_eq {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : a + b = n

theorem Matroid.IsFiniteUniform.le_left {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : a ≤ n

theorem Matroid.IsFiniteUniform.le_right {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : b ≤ n

theorem Matroid.IsFiniteUniform.isFiniteUniform_add {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : M.IsFiniteUniform a b

theorem Matroid.IsFiniteUniform.congr₃ {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) {m : ℕ} (hm : m = a + b) : M.IsFiniteUniform a b m

@[simp]

theorem Matroid.IsFiniteUniform.sub_eq_left {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : n - a = b

@[simp]

theorem Matroid.IsFiniteUniform.sub_eq_right {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : n - b = a

theorem Matroid.IsFiniteUniform.loopless_iff {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : M.Loopless ↔ a = 0 → b = 0

theorem Matroid.IsFiniteUniform.simple_iff {α : Type u_1} {M : Matroid α} {a b n : ℕ} (h : M.IsFiniteUniform a b n) : M.Simple ↔ a ≤ 1 → b = 0

theorem Matroid.IsUniform.exists_isFiniteUniform_of_finite {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) [M.Finite] : ∃ (a : ℕ) (b : ℕ) (n : ℕ), M.IsFiniteUniform a b n ∧ ↑a = M.eRank ∧ ↑b = M✶.eRank ∧ ↑n = M.E.encard

theorem Matroid.IsUniform.exists_isFiniteUniform_of_finite' {α : Type u_1} {M : Matroid α} (hM : M.IsUniform) [M.Finite] : ∃ (a : ℕ) (b : ℕ), M.IsFiniteUniform a b ∧ ↑a = M.eRank ∧ ↑b = M✶.eRank

theorem Matroid.IsFiniteRankUniform.exists_isFiniteUniform_of_finite {α : Type u_1} {M : Matroid α} {a : ℕ} (h : M.IsFiniteRankUniform a) [M.Finite] : ∃ (b : ℕ) (n : ℕ), M.IsFiniteUniform a b n ∧ ↑b = M✶.eRank ∧ ↑n = M.E.encard

theorem Matroid.isFiniteUniform_dual_iff {α : Type u_1} {M : Matroid α} {a b n : ℕ} : M✶.IsFiniteUniform a b n ↔ M.IsFiniteUniform b a n

theorem Matroid.IsFiniteUniform.dual {α : Type u_1} {M : Matroid α} {a b n : ℕ} : M.IsFiniteUniform b a n → M✶.IsFiniteUniform a b n

Alias of the reverse direction of Matroid.isFiniteUniform_dual_iff.

theorem Matroid.IsFiniteUniform.of_dual {α : Type u_1} {M : Matroid α} {a b n : ℕ} : M✶.IsFiniteUniform a b n → M.IsFiniteUniform b a n

Alias of the forward direction of Matroid.isFiniteUniform_dual_iff.

theorem Matroid.IsFiniteUniform.dual' {α : Type u_1} {M : Matroid α} {a b : ℕ} (h : M.IsFiniteUniform a b) : M✶.IsFiniteUniform b a

theorem Matroid.isFiniteUniform_unifOn {α : Type u_1} {E : Set α} (hE : E.Finite) (a : ℕ) (haE : ↑a ≤ E.encard) : ∃ (b : ℕ) (n : ℕ), (unifOn E a).IsFiniteUniform a b n ∧ ↑n = E.encard

theorem Matroid.IsFiniteUniform.dual_eq_self {α : Type u_1} {M : Matroid α} {a b : ℕ} (h : M.IsFiniteUniform a a b) : M✶ = M

theorem Matroid.IsFiniteUniform.bDual_eq_self {α : Type u_1} {M : Matroid α} {a b : ℕ} (h : M.IsFiniteUniform a a b) (d : Bool) : M.bDual d = M

theorem Matroid.IsFiniteUniform.contractElem {α : Type u_1} {M : Matroid α} {e : α} {a b n : ℕ} (h : M.IsFiniteUniform (a + 1) b (n + 1)) (he : e ∈ M.E) : (M.contract {e}).IsFiniteUniform a b n

theorem Matroid.IsFiniteUniform.deleteElem {α : Type u_1} {M : Matroid α} {e : α} {a b n : ℕ} (h : M.IsFiniteUniform a (b + 1) (n + 1)) (he : e ∈ M.E) : (M.delete {e}).IsFiniteUniform a b n

theorem Matroid.IsFiniteUniform.contractElem' {α : Type u_1} {M : Matroid α} {e : α} {a b : ℕ} (h : M.IsFiniteUniform (a + 1) b) (he : e ∈ M.E) : (M.contract {e}).IsFiniteUniform a b

theorem Matroid.IsFiniteUniform.deleteElem' {α : Type u_1} {M : Matroid α} {e : α} {a b : ℕ} (h : M.IsFiniteUniform a (b + 1)) (he : e ∈ M.E) : (M.delete {e}).IsFiniteUniform a b

theorem Matroid.IsFiniteUniform.nonempty_iso_unif {α : Type u_1} {M : Matroid α} {a b n : ℕ} (hM : M.IsFiniteUniform a b n) : Nonempty (M ≂ unif a n)

theorem Matroid.IsFiniteUniform.exists_eq_circuitOn {α : Type u_1} {M : Matroid α} {a n : ℕ} (hM : M.IsFiniteUniform a 1 n) : ∃ (E : Set α), E.Nonempty ∧ E.Finite ∧ M = circuitOn E

theorem Matroid.IsFiniteUniform.nonempty_iso {α : Type u_1} {M : Matroid α} {a b n : ℕ} (hM : M.IsFiniteUniform a b n) {β : Type u_2} {N : Matroid β} {m : ℕ} (hN : N.IsFiniteUniform a b m) : Nonempty (M ≂ N)

Two finite uniform matroids with the same parameters are isomorphic.

theorem Matroid.IsFiniteUniform.of_iso {α : Type u_1} {M : Matroid α} {a b n : ℕ} (hM : M.IsFiniteUniform a b n) {β : Type u_2} {N : Matroid β} (e : M ≂ N) : N.IsFiniteUniform a b n

theorem Matroid.Iso.isFiniteUniform_iff {α : Type u_1} {M : Matroid α} {a b n : ℕ} {β : Type u_2} {N : Matroid β} (e : M ≂ N) : M.IsFiniteUniform a b n ↔ N.IsFiniteUniform a b n

theorem Matroid.IsUniform.exists_eq_unifOn {α : Type u_1} {M : Matroid α} [M.RankFinite] (hM : M.IsUniform) : ∃ (E : Set α) (k : ℕ), ↑k ≤ E.encard ∧ M = unifOn E k ∧ M.eRank = ↑k

A finite-rank uniform matroid is one of the obvious ones - maybe use IsFiniteRankUniform instead

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

theorem Matroid.IsUniform.exists_eq_unifOn_of_finitary {α : Type u_1} {M : Matroid α} [M.Finitary] [M✶.RankPos] (hM : M.IsUniform) : ∃ (E : Set α) (k : ℕ), ↑k ≤ E.encard ∧ M = unifOn E k ∧ M.eRank = ↑k

A finitary non-free uniform matroid is one of the obvious ones. maybe use IsFiniteRankUniform instead

theorem Matroid.IsUniform.exists_eq_freeOn_or_unifOn_of_finitary {α : Type u_1} {M : Matroid α} [M.Finitary] (hM : M.IsUniform) : ∃ (E : Set α), M = freeOn E ∨ ∃ (k : ℕ), ↑k ≤ E.encard ∧ M = unifOn E k ∧ M.eRank = ↑k

Don't use.

theorem Matroid.isUniform_of_eRank_add_one_le_girth {α : Type u_1} {M : Matroid α} [M.RankFinite] (hM : M.eRank + 1 ≤ M.girth) : M.IsUniform

theorem Matroid.isUniform_of_eRank_lt_girth {α : Type u_1} {M : Matroid α} (hM : M.eRank < M.girth) : M.IsUniform

theorem Matroid.nonempty_iso_unif_iff' {α : Type u_1} {M : Matroid α} {a b : ℕ} : Nonempty (M ≂ unif a (a + b)) ↔ M.IsFiniteUniform a b

theorem Matroid.nonempty_iso_unif_iff {α : Type u_1} {M : Matroid α} {a b : ℕ} (hab : a ≤ b) : Nonempty (M ≂ unif a b) ↔ M.IsFiniteRankUniform a ∧ M.E.encard = ↑b

theorem Matroid.nonempty_iso_unif_iff'' {α : Type u_1} {M : Matroid α} {a b : ℕ} : Nonempty (M ≂ unif a b) ↔ M.IsFiniteRankUniform (min a b) ∧ M.E.encard = ↑b

theorem Matroid.nonempty_iso_unif_iff''' {α : Type u_1} {M : Matroid α} {a b : ℕ} : Nonempty (M ≂ unif a b) ↔ ∃ (E : Set α), M = unifOn E a ∧ E.encard = ↑b

theorem Matroid.eq_unifOn_of_eRank_le_one {α : Type u_1} {M : Matroid α} [M.Loopless] (hM : M.eRank ≤ 1) : ∃ (E : Set α), M = unifOn E 1

theorem Matroid.isFiniteRankUniform_of_eRank_le_one {α : Type u_1} {M : Matroid α} [M.Loopless] [M.Nonempty] (hM : M.eRank ≤ 1) : M.IsFiniteRankUniform 1

theorem Matroid.eq_unifOn_of_eRank_le_two {α : Type u_1} {M : Matroid α} [M.Simple] (hM : M.eRank ≤ 2) : ∃ (E : Set α), M = unifOn E 2

theorem Matroid.eq_unifOn_two_iff {α : Type u_1} {M : Matroid α} {E : Set α} : M = unifOn E 2 ↔ M.E = E ∧ M.eRank ≤ 2 ∧ M.Simple

theorem Matroid.isFiniteRankUniform_of_eRank_le_two {α : Type u_1} {M : Matroid α} [M.Simple] (hM : M.eRank ≤ 2) (hnt : M.E.Nontrivial) : M.IsFiniteRankUniform 2

@[simp]

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

theorem Matroid.nonempty_iso_line_iff {α : Type u_1} {M : Matroid α} {n : ℕ} : Nonempty (M ≂ unif 2 n) ↔ M.Simple ∧ M.eRank ≤ 2 ∧ M.E.encard = ↑n

theorem Matroid.eRank_le_one_iff {α : Type u_1} {M : Matroid α} : M.eRank ≤ 1 ↔ ∃ (E₀ : Set α) (E₁ : Set α) (h : Disjoint E₀ E₁), M = (loopyOn E₀).disjointSum (unifOn E₁ 1) h