Commit 2024-04-16 11:34 41ebfad3

View on Github →

feat: Matroid restrictions (#9023) We define the restriction of a matroid to a set, the resulting partial order on the set of matroids on a type, and give associated API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matroid/Basic.lean

added theorem Matroid.Basis'.inter_eq_of_subset_indep

added theorem Matroid.Basis'.mem_of_insert_indep

added theorem Matroid.exists_basis_disjoint_basis_of_subset

added theorem Matroid.finite_setOf_matroid'

added theorem Matroid.finite_setOf_matroid

Created Mathlib/Data/Matroid/Restrict.lean

added theorem Matroid.Base.basis_of_restriction

added theorem Matroid.Basis'.encard_eq_encard

added theorem Matroid.Basis.base_of_base_subset

added theorem Matroid.Basis.base_restrict

added theorem Matroid.Basis.basis_of_basis_of_subset_of_subset

added theorem Matroid.Basis.basis_restrict_of_subset

added theorem Matroid.Basis.basis_restriction

added theorem Matroid.Basis.encard_eq_encard

added theorem Matroid.Basis.eq_exchange_of_diff_eq_singleton

added theorem Matroid.Basis.exchange

added theorem Matroid.Basis.of_restriction

added theorem Matroid.Basis.restrict_base

added theorem Matroid.Basis.transfer

added theorem Matroid.Dep.dep_restriction

added theorem Matroid.Dep.of_restriction

added theorem Matroid.Indep.augment

added theorem Matroid.Indep.exists_basis_subset_union_basis

added theorem Matroid.Indep.exists_insert_of_not_basis

added theorem Matroid.Indep.indep_restrict_of_subset

added theorem Matroid.Indep.indep_restriction

added theorem Matroid.Indep.of_restrict

added theorem Matroid.Indep.of_restriction

added theorem Matroid.Matroidᵣ.coe_inj

added structure Matroid.Matroidᵣ

added theorem Matroid.Restriction.antisymm

added theorem Matroid.Restriction.eq_or_strictRestriction

added theorem Matroid.Restriction.eq_restrict

added theorem Matroid.Restriction.exists_eq_restrict

added theorem Matroid.Restriction.finitary

added theorem Matroid.Restriction.finite

added theorem Matroid.Restriction.finiteRk

added theorem Matroid.Restriction.of_subset

added theorem Matroid.Restriction.refl

added theorem Matroid.Restriction.strictRestriction_of_ground_ne

added theorem Matroid.Restriction.strictRestriction_of_ne

added theorem Matroid.Restriction.subset

added theorem Matroid.Restriction.trans

added def Matroid.Restriction

added theorem Matroid.StrictRestriction.eq_restrict

added theorem Matroid.StrictRestriction.exists_eq_restrict

added theorem Matroid.StrictRestriction.irrefl

added theorem Matroid.StrictRestriction.ne

added theorem Matroid.StrictRestriction.of_ssubset

added theorem Matroid.StrictRestriction.restriction

added theorem Matroid.StrictRestriction.ssubset

added def Matroid.StrictRestriction

added theorem Matroid.base_restrict_iff'

added theorem Matroid.base_restrict_iff

added theorem Matroid.basis'_restrict_iff

added theorem Matroid.basis_restrict_iff'

added theorem Matroid.basis_restrict_iff

added theorem Matroid.finite_setOf_restriction

added theorem Matroid.ofMatroid_le_iff

added theorem Matroid.ofMatroid_lt_iff

added def Matroid.restrict

added def Matroid.restrictIndepMatroid

added theorem Matroid.restrict_dep_iff

added theorem Matroid.restrict_eq_restrict_iff

added theorem Matroid.restrict_eq_self_iff

added theorem Matroid.restrict_finite

added theorem Matroid.restrict_ground_eq

added theorem Matroid.restrict_ground_eq_self

added theorem Matroid.restrict_idem

added theorem Matroid.restrict_indep_iff

added theorem Matroid.restrict_restrict_eq

added theorem Matroid.restrict_restriction

added theorem Matroid.restrict_strictRestriction

added theorem Matroid.restriction_iff_exists