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

• Matroid.unif_isoMinor_contr a b d = ⋯.mp (⋯.mp (⋯.mp (Matroid.unif_isoRestr_unif (b - a) ⋯).isoMinor.dual))

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

theorem Matroid.IsFiniteRankUniform.nonempty_isoMinor_iff {α : Type u_1} {a : ℕ} {β : Type u_2} {M : Matroid β} {N : Matroid α} (hN : N.IsFiniteRankUniform a) : Nonempty (IsoMinor N M) ↔ ∃ (C : Set β) (X : Set β), M.Indep C ∧ (M.contract C).IsFiniteRankUniformOn a X ∧ Nonempty (↑N.E ≃ ↑X)

theorem Matroid.nonempty_loopyOn_isoMinor_iff {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} : Nonempty (IsoMinor (loopyOn E) M) ↔ ∃ (f : ↑E ↪ β), M.Coindep (Set.range ⇑f)

theorem Matroid.nonempty_freeOn_isoMinor_iff {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} : Nonempty (IsoMinor (freeOn E) M) ↔ ∃ (f : ↑E ↪ β), M.Indep (Set.range ⇑f)

theorem Matroid.nonempty_freeOn_isoMinor_iff_of_finite {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} (hEfin : E.Finite) : Nonempty (IsoMinor (freeOn E) M) ↔ E.encard ≤ M.eRank

theorem Matroid.nonempty_loopyOn_isoMinor_iff_of_finite {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} (hEfin : E.Finite) : Nonempty (IsoMinor (loopyOn E) M) ↔ E.encard ≤ M✶.eRank

theorem Matroid.nonempty_circuitOn_isoMinor_iff {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} (he : E.Nonempty) : Nonempty (IsoMinor (circuitOn E) M) ↔ ∃ (C : Set β), M.IsCircuit C ∧ Nonempty (↑E ↪ ↑C)

theorem Matroid.nonempty_circuitOn_isoMinor_iff_of_finite {α : Type u_1} {β : Type u_2} {E : Set α} {M : Matroid β} (he : E.Nonempty) (hEfin : E.Finite) : Nonempty (IsoMinor (circuitOn E) M) ↔ ∃ (C : Set β), M.IsCircuit C ∧ E.encard ≤ C.encard

theorem Matroid.IsFiniteUniform.nonempty_isoMinor_iff {α : Type u_1} {M : Matroid α} {a b n : ℕ} {β : Type u_2} {N : Matroid β} {a' b' n' : ℕ} (hM : M.IsFiniteUniform a b n) (hN : N.IsFiniteUniform a' b' n') : Nonempty (IsoMinor N M) ↔ a' ≤ a ∧ b' ≤ b