theorem Matroid.Indep.mono {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hY : M.Indep Y) : M.Indep X

theorem Matroid.Nonspanning.mono {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hY : M.Nonspanning Y) : M.Nonspanning X

theorem Matroid.Coindep.mono {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hY : M.Coindep Y) : M.Coindep X