Sort

📁 Source: Mathlib/Data/Finset/Sort.lean

Statistics

Metric	Count
Definitions `instRepr`, `orderEmbOfCardLe`, `orderEmbOfFin`, `orderIsoOfFin`, `sort`, `orderIsoFinOfCardEq`	6
Theorems `sort_univ`, `coe_orderIsoOfFin_apply`, `image_orderEmbOfFin_univ`, `length_sort`, `listMap_orderEmbOfFin_finRange`, `map_orderEmbOfFin_univ`, `map_sort`, `max'_eq_sorted_last`, `mem_sort`, `min'_eq_sorted_zero`, `orderEmbOfCardLe_mem`, `orderEmbOfFin_apply`, `orderEmbOfFin_compl_singleton`, `orderEmbOfFin_compl_singleton_apply`, `orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb`, `orderEmbOfFin_eq_orderEmbOfFin_iff`, `orderEmbOfFin_last`, `orderEmbOfFin_mem`, `orderEmbOfFin_singleton`, `orderEmbOfFin_unique`, `orderEmbOfFin_unique'`, `orderEmbOfFin_zero`, `orderIsoOfFin_symm_apply`, `pairwise_sort`, `range_orderEmbOfFin`, `sort_cons`, `sort_empty`, `sort_eq`, `sort_insert`, `sort_mk`, `sort_nodup`, `sort_perm_toList`, `sort_range`, `sort_singleton`, `sort_sorted`, `sort_sorted_gt`, `sort_sorted_lt`, `sort_toFinset`, `sort_val`, `sortedGT_sort`, `sortedLT_sort`, `sorted_last_eq_max'`, `sorted_last_eq_max'_aux`, `sorted_zero_eq_min'`, `sorted_zero_eq_min'_aux`, `toFinset_sort`, `map_finsetSort`, `nonempty_orderEmbedding_of_finite_infinite`	48
Total	54

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sort_univ` 📖	mathematical	—	`Finset.sort` `Finset.univ` `fintype` `instIsTransLe` `PartialOrder.toPreorder` `instPartialOrder` `instAntisymmLe` `LE.total` `instLinearOrder`	—	`List.SortedLT.eq_of_mem_iff` `instIsTransLe` `instAntisymmLe` `LE.total` `Finset.sortedLT_sort` `List.sortedLT_finRange`

Finset

Definitions

Name	Category	Theorems
`instRepr` 📖	CompOp	—
`orderEmbOfCardLe` 📖	CompOp	1 math math: `orderEmbOfCardLe_mem`
`orderEmbOfFin` 📖	CompOp	26 math math: `Composition.orderEmbOfFin_boundaries`, `image_orderEmbOfFin_univ`, `finSumEquivOfFinset_inr`, `orderEmbOfFin_unique`, `orderEmbOfFin_eq_orderEmbOfFin_iff`, `coe_orderIsoOfFin_apply`, `orderEmbOfFin_zero`, `orderEmbOfFin_last`, `Affine.Simplex.face_points`, `range_orderEmbOfFin`, `orderEmbOfFin_singleton`, `Set.powersetCard.ofFinEmbEquiv_symm_apply`, `orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb`, `orderEmbOfFin_unique'`, `orderEmbOfFin_apply`, `intervalGapsWithin_snd_of_lt`, `intervalGapsWithin_succ_fst_of_lt`, `intervalGapsWithin_fst_of_lt_lt`, `map_orderEmbOfFin_univ`, `Nat.nth_eq_orderEmbOfFin`, `Affine.Simplex.face_points'`, `orderEmbOfFin_mem`, `listMap_orderEmbOfFin_finRange`, `finSumEquivOfFinset_inl`, `orderEmbOfFin_compl_singleton_apply`, `orderEmbOfFin_compl_singleton`
`orderIsoOfFin` 📖	CompOp	2 math math: `orderIsoOfFin_symm_apply`, `coe_orderIsoOfFin_apply`
`sort` 📖	CompOp	29 math math: `sort_empty`, `sortedGT_sort`, `orderIsoOfFin_symm_apply`, `mem_sort`, `sort_eq`, `List.toFinset_sort`, `pairwise_sort`, `sort_range`, `sort_mk`, `max'_eq_sorted_last`, `sort_sorted_lt`, `sort_nodup`, `sort_sorted`, `min'_eq_sorted_zero`, `sortedLT_sort`, `orderEmbOfFin_apply`, `sort_insert`, `sort_cons`, `sort_sorted_gt`, `Fin.sort_univ`, `sort_toFinset`, `Nat.nth_eq_getD_sort`, `length_sort`, `StrictMonoOn.map_finsetSort`, `map_sort`, `sort_perm_toList`, `listMap_orderEmbOfFin_finRange`, `sort_singleton`, `sort_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_orderIsoOfFin_apply` 📖	mathematical	`card`	`Finset` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderIso` `orderIsoOfFin` `OrderEmbedding` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	—
`image_orderEmbOfFin_univ` 📖	mathematical	`card`	`image` `LinearOrder.toDecidableEq` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `univ` `Fin.fintype`	—	`coe_injective` `coe_image` `coe_univ` `Set.image_univ` `range_orderEmbOfFin`
`length_sort` 📖	mathematical	—	`sort` `card`	—	`Multiset.length_sort`
`listMap_orderEmbOfFin_finRange` 📖	mathematical	`card`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `sort` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `length_sort`
`map_orderEmbOfFin_univ` 📖	mathematical	`card`	`map` `RelEmbedding.toEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderEmbOfFin` `univ` `Fin.fintype`	—	`map_eq_image` `image_orderEmbOfFin_univ`
`map_sort` 📖	mathematical	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`sort` `map`	—	`Multiset.map_sort`
`max'_eq_sorted_last` 📖	mathematical	`Nonempty`	`max'` `sort` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `length_sort` `card_pos` `sorted_last_eq_max'_aux`
`mem_sort` 📖	mathematical	—	`sort` `Finset` `instMembership`	—	`Multiset.mem_sort`
`min'_eq_sorted_zero` 📖	mathematical	`Nonempty`	`min'` `sort` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `sorted_zero_eq_min'_aux`
`orderEmbOfCardLe_mem` 📖	mathematical	`card`	`Finset` `instMembership` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfCardLe`	—	—
`orderEmbOfFin_apply` 📖	mathematical	`card`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `sort` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	—
`orderEmbOfFin_compl_singleton` 📖	mathematical	`card` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `booleanAlgebra` `Fin.fintype` `instSingleton`	`orderEmbOfFin` `Fin.instLinearOrder` `RelEmbedding.trans` `OrderIso.toOrderEmbedding` `Fin.castOrderIso` `Fin.succAboveOrderEmb`	—	`DFunLike.coe_injective` `card_compl` `Fintype.card_fin` `card_singleton` `orderEmbOfFin_unique` `StrictMono.comp` `Fin.strictMono_succAbove` `Fin.cast_strictMono`
`orderEmbOfFin_compl_singleton_apply` 📖	mathematical	`card` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `booleanAlgebra` `Fin.fintype` `instSingleton`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Fin.instLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `Fin.succAbove`	—	`orderEmbOfFin_compl_singleton`
`orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb` 📖	mathematical	—	`orderEmbOfFin` `Fin.instLinearOrder` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `booleanAlgebra` `Fin.fintype` `instSingleton` `Fin.succAboveOrderEmb`	—	`orderEmbOfFin_compl_singleton`
`orderEmbOfFin_eq_orderEmbOfFin_iff` 📖	mathematical	`card`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	`OrderEmbedding.eq_iff_eq`
`orderEmbOfFin_last` 📖	mathematical	`card`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `max'` `Nonempty` `card_pos`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `card_pos` `length_sort` `max'_eq_sorted_last`
`orderEmbOfFin_mem` 📖	mathematical	`card`	`Finset` `instMembership` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	—
`orderEmbOfFin_singleton` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `Finset` `instSingleton` `card_singleton`	—	`card_singleton` `card_pos` `orderEmbOfFin_zero` `singleton_nonempty` `min'_singleton`
`orderEmbOfFin_unique` 📖	mathematical	`card` `Finset` `instMembership` `StrictMono` `PartialOrder.toPreorder` `Fin.instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	`IsWellOrder.toIsWellFounded` `Fin.Lt.isWellOrder` `OrderEmbedding.strictMono` `range_orderEmbOfFin` `Set.image_univ` `coe_univ` `coe_image` `eq_of_subset_of_card_le` `mem_image` `card_image_of_injective` `StrictMono.injective` `card_univ` `Fintype.card_fin` `le_refl`
`orderEmbOfFin_unique'` 📖	mathematical	`card` `Finset` `instMembership` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding`	`orderEmbOfFin`	—	`RelEmbedding.ext` `orderEmbOfFin_unique` `OrderEmbedding.strictMono`
`orderEmbOfFin_zero` 📖	mathematical	`card`	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `min'` `Nonempty` `card_pos`	—	`card_pos` `sorted_zero_eq_min'`
`orderIsoOfFin_symm_apply` 📖	mathematical	`card`	`DFunLike.coe` `OrderIso` `Finset` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoOfFin` `LinearOrder.toDecidableEq` `sort` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	—
`pairwise_sort` 📖	mathematical	—	`sort`	—	`Multiset.pairwise_sort`
`range_orderEmbOfFin` 📖	mathematical	`card`	`Set.range` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin` `SetLike.coe` `Finset` `instSetLike`	—	`Set.range_comp` `RelIso.range_eq` `Set.image_univ` `Subtype.range_coe_subtype`
`sort_cons` 📖	mathematical	`Finset` `instMembership`	`sort` `cons`	—	`sort.eq_1` `cons_val` `Multiset.sort_cons` `sort_val`
`sort_empty` 📖	mathematical	—	`sort` `Finset` `instEmptyCollection`	—	`Multiset.sort_zero`
`sort_eq` 📖	mathematical	—	`Multiset.ofList` `sort` `val`	—	`Multiset.sort_eq`
`sort_insert` 📖	mathematical	`Finset` `instMembership`	`sort` `instInsert`	—	`cons_eq_insert` `sort_cons`
`sort_mk` 📖	mathematical	`Multiset.Nodup`	`sort` `Multiset.sort`	—	—
`sort_nodup` 📖	mathematical	—	`sort`	—	`sort_eq` `nodup`
`sort_perm_toList` 📖	mathematical	—	`sort` `toList`	—	`Multiset.coe_eq_coe` `sort_eq` `coe_toList`
`sort_range` 📖	mathematical	—	`sort` `range` `instIsTransLe` `Nat.instPreorder` `LE.total` `Nat.instLinearOrder`	—	`Multiset.sort_range`
`sort_singleton` 📖	mathematical	—	`sort` `Finset` `instSingleton`	—	`Multiset.sort_singleton`
`sort_sorted` 📖	mathematical	—	`sort`	—	`pairwise_sort`
`sort_sorted_gt` 📖	mathematical	—	`List.SortedGT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sort` `Preorder.toLE` `LinearOrder.toDecidableLE` `instIsTransGe` `instAntisymmGe` `LE.total'`	—	`sortedGT_sort`
`sort_sorted_lt` 📖	mathematical	—	`List.SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sort` `Preorder.toLE` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	`sortedLT_sort`
`sort_toFinset` 📖	mathematical	—	`List.toFinset` `sort`	—	`sort_nodup` `eq_of_veq` `sort_eq` `List.toFinset_eq`
`sort_val` 📖	mathematical	—	`Multiset.sort` `val` `sort`	—	—
`sortedGT_sort` 📖	mathematical	—	`List.SortedGT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sort` `Preorder.toLE` `LinearOrder.toDecidableLE` `instIsTransGe` `instAntisymmGe` `LE.total'`	—	`List.SortedGE.sortedGT_of_nodup` `instIsTransGe` `instAntisymmGe` `LE.total'` `List.Pairwise.sortedGE` `pairwise_sort` `sort_nodup`
`sortedLT_sort` 📖	mathematical	—	`List.SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sort` `Preorder.toLE` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	—	`List.SortedLE.sortedLT_of_nodup` `instIsTransLe` `instAntisymmLe` `LE.total` `List.Pairwise.sortedLE` `pairwise_sort` `sort_nodup`
`sorted_last_eq_max'` 📖	mathematical	`sort` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	`max'`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `sorted_last_eq_max'_aux`
`sorted_last_eq_max'_aux` 📖	mathematical	`sort` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total` `Nonempty`	`max'`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `le_antisymm` `mem_sort` `le_max'` `max'_mem` `List.Pairwise.rel_get_of_le` `instReflLe` `pairwise_sort` `Fin.prop`
`sorted_zero_eq_min'` 📖	mathematical	`sort` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total`	`min'` `card` `Nonempty` `card_pos`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `sorted_zero_eq_min'_aux` `card_pos`
`sorted_zero_eq_min'_aux` 📖	mathematical	`sort` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total` `Nonempty`	`min'`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `le_antisymm` `mem_sort` `min'_mem` `List.Pairwise.rel_get_of_le` `instReflLe` `pairwise_sort` `min'_le`

Fintype

Definitions

Name	Category	Theorems
`orderIsoFinOfCardEq` 📖	CompOp	—

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFinset_sort` 📖	mathematical	—	`Finset.sort` `toFinset`	—	`Finset.pairwise_sort` `Perm.eq_of_pairwise'` `Finset.sort_perm_toList` `toFinset_toList`

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_finsetSort` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.sort` `Preorder.toLE` `LinearOrder.toDecidableLE` `instIsTransLe` `instAntisymmLe` `LE.total` `Finset.map`	—	`Finset.map_sort` `instIsTransLe` `instAntisymmLe` `LE.total` `le_iff_le`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_orderEmbedding_of_finite_infinite` 📖	mathematical	—	`OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Infinite.exists_subset_card_eq`

---

← Back to Index