Basic stuff about matroids

This file provides lemmas about matroids that are not present in Mathlib.

@[reducible, inline]

abbrev Disjoint.matroidSum {α : Type u_1} {Mₗ Mᵣ : Matroid α} (hEE : Mₗ.E ⫗ Mᵣ.E) : Matroid α

The sum of two matroids on disjoint ground sets of the same type is a matroid whose ground set is a union of the ground sets of the summands, in which a subset of said ground set is independent iff its intersections with respective ground set are independent in each matroid.

Equations

• hEE.matroidSum = Mₗ.disjointSum Mᵣ hEE

theorem Matroid.IsBase.not_ssubset_indep {α : Type u_1} {M : Matroid α} {G I : Set α} (hMG : M.IsBase G) (hMI : M.Indep I) : ¬G ⊂ I

theorem Matroid.Indep.finite_of_finite_base {α : Type u_1} {M : Matroid α} {G I : Set α} (hMI : M.Indep I) (hMG : M.IsBase G) (hG : Finite ↑G) : Finite ↑I