noncomputable def Matroid.unif_isoRestr_unif {b b' : ℕ} (a : ℕ) (hbb' : b ≤ b') : IsoRestr (unif a b) (unif a b')

Equations

• Matroid.unif_isoRestr_unif a hbb' = ⋯.some.symm.isoRestr.trans ⋯.isoRestr

noncomputable def Matroid.unif_isoMinor_contr (a b d : ℕ) : IsoMinor (unif a b) (unif (a + d) (b + d))

Equations

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

theorem Matroid.unif_isoMinor_unif_iff {a₁ a₂ d₁ d₂ : ℕ} : Nonempty (IsoMinor (unif a₁ (a₁ + d₁)) (unif a₂ (a₂ + d₂))) ↔ a₁ ≤ a₂ ∧ d₁ ≤ d₂

theorem Matroid.unif_isoMinor_unif_iff' {a₁ a₂ b₁ b₂ : ℕ} (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) : Nonempty (IsoMinor (unif a₁ b₁) (unif a₂ b₂)) ↔ a₁ ≤ a₂ ∧ b₁ - a₁ ≤ b₂ - a₂

theorem Matroid.unif_isoRestr_unifOn {α : Type u_1} {E : Set α} {b a : ℕ} (hbb : ↑b ≤ E.encard) : Nonempty (IsoRestr (unif a b) (unifOn E a))

def Matroid.NoUniformMinor {α : Type u_1} (M : Matroid α) (a b : ℕ) : Prop

Equations

• M.NoUniformMinor a b = IsEmpty (Matroid.IsoMinor (Matroid.unif a b) M)

@[simp]

theorem Matroid.not_noUniformMinor_iff {α : Type u_1} {M : Matroid α} {a b : ℕ} : ¬M.NoUniformMinor a b ↔ Nonempty (IsoMinor (unif a b) M)

theorem Matroid.NoUniformMinor.minor {α : Type u_1} {M N : Matroid α} {a b : ℕ} (hM : M.NoUniformMinor a b) (hNM : N ≤m M) : N.NoUniformMinor a b

theorem Matroid.nonempty_unif_isoRestr_unifOn {α : Type u_1} (a : ℕ) {b : ℕ} {E : Set α} (h : ↑b ≤ E.encard) : Nonempty (IsoRestr (unif a b) (unifOn E a))

@[simp]

theorem Matroid.unifOn_noUniformMinor_iff {α : Type u_1} {E : Set α} {a b : ℕ} : (unifOn E a).NoUniformMinor a b ↔ E.encard < ↑b

theorem Matroid.no_line_minor_iff_of_eRank_le_two {α : Type u_1} {M : Matroid α} {b : ℕ} (hM : M.eRank ≤ 2) : M.NoUniformMinor 2 b ↔ M.simplification.E.encard < ↑b

theorem Matroid.NoUniformMinor.le_minor {α : Type u_1} {M : Matroid α} {a b b' : ℕ} (hM : M.NoUniformMinor a b) (ha : a ≤ b) (hb' : b ≤ b') : M.NoUniformMinor a b'

theorem Matroid.NoUniformMinor.lt_of_isoMinor {α : Type u_1} {M : Matroid α} {β : Type u_2} {N : Matroid β} {a b : ℕ} (h : M.NoUniformMinor a b) (hNM : IsoMinor N M) (hN : N.IsFiniteRankUniform a) : N.E.encard < ↑b

@[simp]

theorem Matroid.noUniformMinor_self_iff {α : Type u_1} {M : Matroid α} {a : ℕ} : M.NoUniformMinor a a ↔ M.eRank < ↑a