FiniteExhaustion

📁 Source: Mathlib/Data/Set/FiniteExhaustion.lean

Statistics

Metric	Count
Definitions finiteExhaustion, FiniteExhaustion, instFunLikeNat, prod, toFun	5
Theorems nonempty_finiteExhaustion_iff, finite, finite', iUnion_eq, iUnion_eq', instFiniteElemCoeNat, instRelHomClassNatLeSubset, mono, prod_apply, subset_succ, subset_succ', toFun_eq_coe	12
Total	17

Set

Definitions

Name	Category	Theorems
FiniteExhaustion 📖	CompData	9 math math: FiniteExhaustion.instFiniteElemCoeNat, FiniteExhaustion.mono, FiniteExhaustion.Set.nonempty_finiteExhaustion_iff, FiniteExhaustion.subset_succ, FiniteExhaustion.instRelHomClassNatLeSubset, FiniteExhaustion.finite, FiniteExhaustion.iUnion_eq, FiniteExhaustion.toFun_eq_coe, FiniteExhaustion.prod_apply

Set.Countable

Definitions

Name	Category	Theorems
finiteExhaustion 📖	CompOp	—

Set.FiniteExhaustion

Definitions

Name	Category	Theorems
instFunLikeNat 📖	CompOp	8 math math: instFiniteElemCoeNat, mono, subset_succ, instRelHomClassNatLeSubset, finite, iUnion_eq, toFun_eq_coe, prod_apply
prod 📖	CompOp	1 math math: prod_apply
toFun 📖	CompOp	4 math math: subset_succ', iUnion_eq', finite', toFun_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite 📖	mathematical	—	Set.Finite DFunLike.coe Set.FiniteExhaustion Set instFunLikeNat	—	finite'
finite' 📖	mathematical	—	Finite Set.Elem toFun	—	—
iUnion_eq 📖	mathematical	—	Set.iUnion DFunLike.coe Set.FiniteExhaustion Set instFunLikeNat	—	iUnion_eq'
iUnion_eq' 📖	mathematical	—	Set.iUnion toFun	—	—
instFiniteElemCoeNat 📖	mathematical	—	Finite Set.Elem DFunLike.coe Set.FiniteExhaustion Set instFunLikeNat	—	finite'
instRelHomClassNatLeSubset 📖	mathematical	—	RelHomClass Set.FiniteExhaustion Set Set.instHasSubset instFunLikeNat	—	monotone_nat_of_le_succ subset_succ'
mono 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe Set.FiniteExhaustion instFunLikeNat	—	OrderHomClass.mono instRelHomClassNatLeSubset
prod_apply 📖	mathematical	—	DFunLike.coe Set.FiniteExhaustion SProd.sprod Set Set.instSProd instFunLikeNat prod	—	—
subset_succ 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe Set.FiniteExhaustion instFunLikeNat	—	subset_succ'
subset_succ' 📖	mathematical	—	Set Set.instHasSubset toFun	—	—
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe Set.FiniteExhaustion Set instFunLikeNat	—	—

Set.FiniteExhaustion.Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_finiteExhaustion_iff 📖	mathematical	—	Set.FiniteExhaustion Set.Countable	—	Set.FiniteExhaustion.iUnion_eq Set.countable_iUnion instCountableNat Set.Finite.countable Set.FiniteExhaustion.finite

---

← Back to Index