structure Matroid.WeakLE {α : Type u_1} (N M : Matroid α) : Prop

• forall_indep_of_indep (I : Set α) : N.Indep I → M.Indep I
• ground_eq : N.E = M.E

theorem Matroid.weakLE_iff {α : Type u_1} (N M : Matroid α) : N ≤w M ↔ (∀ (I : Set α), N.Indep I → M.Indep I) ∧ N.E = M.E

def Matroid.«term_≤w_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_≤w_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤w_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤w ") (Lean.ParserDescr.cat `term 51))

theorem Matroid.WeakLE.ground_eq_of_dual {α : Type u_1} {M N : Matroid α} (h : N✶ ≤w M✶) : N.E = M.E

theorem Matroid.WeakLE.subset_ground_of_subset_ground_left {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N ≤w M) (hX : X ⊆ N.E := by aesop_mat) : X ⊆ M.E

theorem Matroid.WeakLE.subset_ground_of_subset_ground_right {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N ≤w M) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ N.E

theorem Matroid.WeakLE.indep_of_indep {α : Type u_1} {M N : Matroid α} {I : Set α} (h : N ≤w M) (hI : N.Indep I) : M.Indep I

theorem Matroid.WeakLE.spanning_of_spanning_of_dual {α : Type u_1} {M N : Matroid α} {S : Set α} (h : N✶ ≤w M✶) (hS : N.Spanning S) : M.Spanning S

theorem Matroid.WeakLE.nonspanning_of_nonspanning_of_dual {α : Type u_1} {M N : Matroid α} {S : Set α} (h : N✶ ≤w M✶) (hS : M.Nonspanning S) : N.Nonspanning S

theorem Matroid.WeakLE.dep_of_dep {α : Type u_1} {M N : Matroid α} {D : Set α} (h : N ≤w M) (hD : M.Dep D) : N.Dep D

theorem Matroid.weakLE_iff_forall_dep_of_dep {α : Type u_1} {M N : Matroid α} : N ≤w M ↔ N.E = M.E ∧ ∀ (D : Set α), M.Dep D → N.Dep D

theorem Matroid.weakLE_of_forall_not_indep_of_isCircuit {α : Type u_1} {M N : Matroid α} (hE : N.E = M.E) (hN : ∀ (C : Set α), M.IsCircuit C → ¬N.Indep C) : N ≤w M

theorem Matroid.WeakLE.refl {α : Type u_1} (M : Matroid α) : M ≤w M

theorem Matroid.WeakLE.antisymm {α : Type u_1} {M N : Matroid α} (h : N ≤w M) (h' : M ≤w N) : N = M

theorem Matroid.WeakLE.trans {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁ ≤w M₂) (h' : M₂ ≤w M₃) : M₁ ≤w M₃

theorem Matroid.WeakLE.delete {α : Type u_1} {M N : Matroid α} (h : N ≤w M) (D : Set α) : N.delete D ≤w M.delete D

theorem Matroid.WeakLE.loops_subset_loops {α : Type u_1} {M N : Matroid α} (h : N ≤w M) : M.loops ⊆ N.loops

theorem Matroid.contract_weakLE_delete {α : Type u_1} (M : Matroid α) (X : Set α) : M.contract X ≤w M.delete X

theorem Matroid.WeakLE.exists_isBasis'_subset_isBasis' {α : Type u_1} {M N : Matroid α} (h : N ≤w M) (X : Set α) : ∃ (I : Set α) (J : Set α), N.IsBasis' I X ∧ M.IsBasis' J X ∧ I ⊆ J

theorem Matroid.WeakLE.exists_isBasis_subset_isBasis {α : Type u_1} {M N : Matroid α} (h : N ≤w M) (X : Set α) (hX : X ⊆ M.E) : ∃ (I : Set α) (J : Set α), N.IsBasis I X ∧ M.IsBasis J X ∧ I ⊆ J

theorem Matroid.WeakLE.exists_isBase_subset_isBase {α : Type u_1} {M N : Matroid α} (h : N ≤w M) : ∃ (I : Set α) (J : Set α), N.IsBase I ∧ M.IsBase J ∧ I ⊆ J

theorem Matroid.WeakLE.eRk_le {α : Type u_1} {M N : Matroid α} (h : N ≤w M) (X : Set α) : N.eRk X ≤ M.eRk X

theorem Matroid.WeakLE.eRank_le {α : Type u_1} {M N : Matroid α} (h : N ≤w M) : N.eRank ≤ M.eRank