Commit 2025-02-13 11:34 b942da74

View on Github →

feat(Data/Matroid/Rank): finite-rank sets in matroids (#21694) We add a new file with API for an IsRkFinite predicate on sets in a matroid, stating that a set has a finite basis. This property is closed under subsets and finite unions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matroid/Rank/Cardinal.lean

added theorem Matroid.isRkFinite_iff_cRk_lt_aleph0

Created Mathlib/Data/Matroid/Rank/Finite.lean

added theorem Matroid.Basis'.finite_iff_isRkFinite

added theorem Matroid.Basis'.isRkFinite_of_finite

added theorem Matroid.Basis.finite_iff_isRkFinite

added theorem Matroid.Basis.isRkFinite_of_finite

added theorem Matroid.Indep.finite_of_subset_isRkFinite

added theorem Matroid.Indep.isRkFinite_iff_finite

added theorem Matroid.Indep.subset_finite_basis'_of_subset_of_isRkFinite

added theorem Matroid.Indep.subset_finite_basis_of_subset_of_isRkFinite

added theorem Matroid.IsRkFinite.closure

added theorem Matroid.IsRkFinite.diff

added theorem Matroid.IsRkFinite.diff_singleton_iff

added theorem Matroid.IsRkFinite.empty

added theorem Matroid.IsRkFinite.exists_finite_basis'

added theorem Matroid.IsRkFinite.exists_finset_basis'

added theorem Matroid.IsRkFinite.finite_of_basis'

added theorem Matroid.IsRkFinite.finite_of_basis

added theorem Matroid.IsRkFinite.finite_of_indep_subset

added theorem Matroid.IsRkFinite.iUnion

added theorem Matroid.IsRkFinite.insert

added theorem Matroid.IsRkFinite.inter_ground

added theorem Matroid.IsRkFinite.inter_left

added theorem Matroid.IsRkFinite.inter_right

added theorem Matroid.IsRkFinite.isRkFinite_diff_iff

added theorem Matroid.IsRkFinite.isRkFinite_union_iff

added theorem Matroid.IsRkFinite.rankFinite

added theorem Matroid.IsRkFinite.subset

added theorem Matroid.IsRkFinite.union

added def Matroid.IsRkFinite

added theorem Matroid.isRkFinite_closure_iff

added theorem Matroid.isRkFinite_ground

added theorem Matroid.isRkFinite_ground_iff_rankFinite

added theorem Matroid.isRkFinite_iff

added theorem Matroid.isRkFinite_iff_exists_basis'

added theorem Matroid.isRkFinite_insert_iff

added theorem Matroid.isRkFinite_inter_ground_iff

added theorem Matroid.isRkFinite_of_finite

added theorem Matroid.isRkFinite_set

added theorem Matroid.isRkFinite_singleton

Modified Mathlib/Data/Matroid/Restrict.lean

added theorem Matroid.Basis'.base_restrict