Finite

📁 Source: Mathlib/Combinatorics/Matroid/Rank/Finite.lean

Statistics

Metric	Count
Definitions Finite, IsRkFinite	2
Theorems finite_of_isRkFinite, finite_of_subset_isRkFinite, isRkFinite_iff_finite, subset_finite_isBasis'_of_subset_of_isRkFinite, subset_finite_isBasis_of_subset_of_isRkFinite, finite_iff_isRkFinite, finite_of_isRkFinite, isRkFinite_of_finite, Finite, finite_iff_isRkFinite, finite_of_isRkFinite, isRkFinite_of_finite, closure, diff, diff_singleton_iff, empty, exists_finite_isBasis', exists_finset_isBasis', finite_of_indep_subset, finite_of_isBasis, finite_of_isBasis', iUnion, insert, inter_ground, inter_left, inter_right, isRkFinite_diff_iff, isRkFinite_union_iff, rankFinite, subset, union, isRkFinite, isRkFinite_closure_iff, isRkFinite_ground, isRkFinite_ground_iff_rankFinite, isRkFinite_iff, isRkFinite_iff_exists_isBasis', isRkFinite_insert_iff, isRkFinite_inter_ground_iff, isRkFinite_of_finite, isRkFinite_set, isRkFinite_singleton	42
Total	44

Matroid

Definitions

Name	Category	Theorems
Finite 📖	CompData	15 math math: instFiniteElemERestrictSubtype, dual_finite, IndepMatroid.ofFinite_finite, finite_of_finite, Finite.loopyOn_finite, finite_emptyOn, instFiniteMapEmbedding, delete_finite, finite_iff, restrict_finite, contract_finite, IsRestriction.finite, instFiniteMap, ofBaseOfFinite_finite, instFiniteMapEquiv
IsRkFinite 📖	MathDef	32 math math: eRk_lt_top_iff, eRk_ne_top_iff, isRkFinite_ground, IsBasis.finite_iff_isRkFinite, isRkFinite_insert_iff, isRkFinite_closure_iff, isRkFinite_iff_cRk_lt_aleph0, RankFinite.isRkFinite, isRkFinite_iff_exists_isBasis', IsBasis.isRkFinite_of_finite, isRkFinite_set, IsRkFinite.isRkFinite_union_iff, IsRkFinite.subset, IsBasis'.finite_iff_isRkFinite, isRkFinite_iff, eRk_eq_top_iff, isRkFinite_ground_iff_rankFinite, IsRkFinite.insert, Indep.isRkFinite_iff_finite, IsRkFinite.union, IsRkFinite.diff_singleton_iff, IsRkFinite.closure, IsBasis'.isRkFinite_of_finite, IsRkFinite.inter_ground, IsRkFinite.empty, IsRkFinite.diff, IsRkFinite.inter_left, IsRkFinite.isRkFinite_diff_iff, isRkFinite_of_finite, isRkFinite_singleton, isRkFinite_inter_ground_iff, IsRkFinite.inter_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRkFinite_closure_iff 📖	mathematical	—	IsRkFinite closure	—	isRkFinite_inter_ground_iff IsRkFinite.subset inter_ground_subset_closure closure_inter_ground IsRkFinite.closure
isRkFinite_ground 📖	mathematical	—	IsRkFinite E	—	isRkFinite_ground_iff_rankFinite
isRkFinite_ground_iff_rankFinite 📖	mathematical	—	IsRkFinite E RankFinite	—	IsRkFinite.eq_1 restrict_ground_eq_self
isRkFinite_iff 📖	mathematical	Set Set.instHasSubset E	IsRkFinite IsBasis Set.Finite	—	isBasis'_iff_isBasis
isRkFinite_iff_exists_isBasis' 📖	mathematical	—	IsRkFinite IsBasis' Set.Finite	—	IsRkFinite.exists_finite_isBasis' IsBasis'.isRkFinite_of_finite
isRkFinite_insert_iff 📖	mathematical	—	IsRkFinite Set Set.instInsert	—	Set.singleton_union IsRkFinite.isRkFinite_union_iff isRkFinite_singleton
isRkFinite_inter_ground_iff 📖	mathematical	—	IsRkFinite Set Set.instInter E	—	exists_isBasis' IsBasis'.isRkFinite_of_finite IsBasis.finite_of_isRkFinite IsBasis'.isBasis_inter_ground IsRkFinite.subset Set.inter_subset_left
isRkFinite_of_finite 📖	mathematical	—	IsRkFinite	—	exists_isBasis' IsBasis'.isRkFinite_of_finite Set.Finite.subset IsBasis'.subset
isRkFinite_set 📖	mathematical	—	IsRkFinite	—	exists_isBasis' IsBasis'.isRkFinite_of_finite Indep.finite IsBasis'.indep
isRkFinite_singleton 📖	mathematical	—	IsRkFinite Set Set.instSingletonSet	—	—

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_isRkFinite 📖	mathematical	Matroid.Indep	Set.Finite	—	isRkFinite_iff_finite
finite_of_subset_isRkFinite 📖	mathematical	Matroid.Indep Set Set.instHasSubset	Set.Finite	—	Matroid.IsRkFinite.finite_of_indep_subset
isRkFinite_iff_finite 📖	mathematical	Matroid.Indep	Matroid.IsRkFinite Set.Finite	—	Matroid.IsBasis.finite_iff_isRkFinite isBasis_self
subset_finite_isBasis'_of_subset_of_isRkFinite 📖	mathematical	Matroid.Indep Set Set.instHasSubset	Matroid.IsBasis' Set.Finite	—	Matroid.IsBasis'.finite_of_isRkFinite subset_isBasis'_of_subset
subset_finite_isBasis_of_subset_of_isRkFinite 📖	mathematical	Matroid.Indep Set Set.instHasSubset Matroid.E	Matroid.IsBasis Set.Finite	—	Matroid.IsBasis.finite_of_isRkFinite subset_isBasis_of_subset

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Finite 📖	mathematical	Matroid.IsBasis	Set.Finite	—	Matroid.Indep.finite indep
finite_iff_isRkFinite 📖	mathematical	Matroid.IsBasis	Set.Finite Matroid.IsRkFinite	—	Matroid.IsBasis'.finite_iff_isRkFinite isBasis'
finite_of_isRkFinite 📖	mathematical	Matroid.IsBasis	Set.Finite	—	finite_iff_isRkFinite
isRkFinite_of_finite 📖	mathematical	Matroid.IsBasis	Matroid.IsRkFinite	—	isBasis'

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_iff_isRkFinite 📖	mathematical	Matroid.IsBasis'	Set.Finite Matroid.IsRkFinite	—	Matroid.IsBase.finite isBase_restrict
finite_of_isRkFinite 📖	mathematical	Matroid.IsBasis'	Set.Finite	—	finite_iff_isRkFinite
isRkFinite_of_finite 📖	mathematical	Matroid.IsBasis'	Matroid.IsRkFinite	—	—

Matroid.IsRkFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	—	Matroid.IsRkFinite Matroid.closure	—	Matroid.exists_isBasis' Matroid.IsBasis.isRkFinite_of_finite Matroid.IsBasis'.isBasis_closure_right Matroid.IsBasis'.finite_of_isRkFinite
diff 📖	mathematical	—	Matroid.IsRkFinite Set Set.instSDiff	—	subset Set.diff_subset
diff_singleton_iff 📖	mathematical	—	Matroid.IsRkFinite Set Set.instSDiff Set.instSingletonSet	—	isRkFinite_diff_iff Matroid.isRkFinite_singleton
empty 📖	mathematical	—	Matroid.IsRkFinite Set Set.instEmptyCollection	—	Matroid.isRkFinite_of_finite Set.finite_empty
exists_finite_isBasis' 📖	mathematical	—	Matroid.IsBasis' Set.Finite	—	Matroid.RankFinite.exists_finite_isBase
exists_finset_isBasis' 📖	mathematical	—	Matroid.IsBasis' SetLike.coe Finset Finset.instSetLike	—	exists_finite_isBasis' Set.Finite.coe_toFinset
finite_of_indep_subset 📖	mathematical	Matroid.Indep Set Set.instHasSubset	Set.Finite	—	Matroid.Indep.finite_of_isRkFinite subset
finite_of_isBasis 📖	mathematical	Matroid.IsBasis	Set.Finite	—	finite_of_isBasis' Matroid.IsBasis.isBasis'
finite_of_isBasis' 📖	mathematical	Matroid.IsBasis'	Set.Finite	—	rankFinite Matroid.IsBase.finite Matroid.isBase_restrict_iff'
iUnion 📖	mathematical	Matroid.IsRkFinite	Set.iUnion	—	Set.finite_iUnion finite_of_isBasis' Matroid.isRkFinite_inter_ground_iff subset closure Matroid.isRkFinite_of_finite Set.iUnion_inter Set.iUnion_subset_iff HasSubset.Subset.trans Set.instIsTransSubset Matroid.IsBasis.subset_closure Matroid.IsBasis'.isBasis_inter_ground Matroid.closure_subset_closure Set.subset_iUnion Matroid.exists_isBasis'
insert 📖	mathematical	—	Matroid.IsRkFinite Set Set.instInsert	—	Set.union_singleton union Matroid.isRkFinite_singleton
inter_ground 📖	mathematical	—	Matroid.IsRkFinite Set Set.instInter Matroid.E	—	Matroid.isRkFinite_inter_ground_iff
inter_left 📖	mathematical	—	Matroid.IsRkFinite Set Set.instInter	—	subset Set.inter_subset_right
inter_right 📖	mathematical	—	Matroid.IsRkFinite Set Set.instInter	—	subset Set.inter_subset_left
isRkFinite_diff_iff 📖	mathematical	—	Matroid.IsRkFinite Set Set.instSDiff	—	isRkFinite_union_iff Set.union_diff_self
isRkFinite_union_iff 📖	mathematical	—	Matroid.IsRkFinite Set Set.instUnion	—	subset Set.subset_union_right union
rankFinite 📖	mathematical	—	Matroid.RankFinite Matroid.restrict	—	—
subset 📖	mathematical	Set Set.instHasSubset	Matroid.IsRkFinite	—	Matroid.exists_isBasis' Matroid.Indep.subset_isBasis'_of_subset Matroid.IsBasis'.indep HasSubset.Subset.trans Set.instIsTransSubset Matroid.IsBasis'.subset Matroid.IsBasis'.isRkFinite_of_finite Set.Finite.subset Matroid.IsBasis'.finite_of_isRkFinite
union 📖	mathematical	—	Matroid.IsRkFinite Set Set.instUnion	—	exists_finite_isBasis' Matroid.isRkFinite_inter_ground_iff subset closure Matroid.isRkFinite_of_finite Set.Finite.union Matroid.closure_union_congr_left Matroid.IsBasis'.closure_eq_closure Matroid.closure_union_congr_right Matroid.inter_ground_subset_closure

Matroid.RankFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRkFinite 📖	mathematical	—	Matroid.IsRkFinite	—	Matroid.restrict_rankFinite

---

← Back to Index