Finset

📁 Source: Mathlib/Order/Fin/Finset.lean

Statistics

Metric	Count
Definitions orderIsoPair, orderIsoSingleton, orderIsoTriple	3
Theorems orderIsoPair_one, orderIsoPair_zero, orderIsoSingleton_apply, orderIsoTriple_one, orderIsoTriple_two, orderIsoTriple_zero	6
Total	9

Fin

Definitions

Name	Category	Theorems
orderIsoPair 📖	CompOp	2 math math: orderIsoPair_zero, orderIsoPair_one
orderIsoSingleton 📖	CompOp	1 math math: orderIsoSingleton_apply
orderIsoTriple 📖	CompOp	3 math math: orderIsoTriple_zero, orderIsoTriple_one, orderIsoTriple_two

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderIsoPair_one 📖	mathematical	Preorder.toLT	Finset SetLike.instMembership Finset.instSetLike Finset.instInsert Finset.instSingleton DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso orderIsoPair	—	—
orderIsoPair_zero 📖	mathematical	Preorder.toLT	Finset SetLike.instMembership Finset.instSetLike Finset.instInsert Finset.instSingleton DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso orderIsoPair	—	—
orderIsoSingleton_apply 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Finset.instSingleton DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso orderIsoSingleton	—	—
orderIsoTriple_one 📖	mathematical	Preorder.toLT	Finset SetLike.instMembership Finset.instSetLike Finset.instInsert Finset.instSingleton DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso orderIsoTriple	—	—
orderIsoTriple_two 📖	mathematical	Preorder.toLT	Finset SetLike.instMembership Finset.instSetLike Finset.instInsert Finset.instSingleton DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso orderIsoTriple	—	—
orderIsoTriple_zero 📖	mathematical	Preorder.toLT	Finset SetLike.instMembership Finset.instSetLike Finset.instInsert Finset.instSingleton DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso orderIsoTriple	—	—

---

← Back to Index