Mathlib Map

Theorems · Definition · combinatorics

Encodable.sortedUniv

(α : Type u_1) → [Fintype α] → [Encodable α] → List α

The elements of a Fintype as a sorted list.

Defined in
Mathlib.Logic.Equiv.Finset
Cited by
5 results in Mathlib
Foundations
Depth 61 from the axioms · uses propext, Quot.sound
Assumes
FintypeEncodable
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.Measure.pi' · cited by 3Measure.pi'MeasureTheory.Measure.pi'_pi · cited by 3Measure.pi'_piEncodable.sortedUniv_nodup · cited by 1Encodable.sortedUniv_nodupEncodable.sortedUniv_toFinset · cited by 1Encodable.sortedUniv_toFi…Encodable.mem_sortedUniv · cited by 1Encodable.mem_sortedUnivEncodable.length_sortedUniv · cited by 0Encodable.length_sortedUn…Encodable.fintypeEquivFin · cited by 0Encodable.fintypeEquivFinDFunLike.coe · cited by 62936DFunLike.coeFintype · cited by 7736FintypeFinset.univ · cited by 3473Finset.univEncodable · cited by 140EncodableFinset.sort · cited by 42Finset.sortOrder.Preimage · cited by 42Order.PreimageEncodable.encode' · cited by 5Encodable.encode'Encodable.sortedUnivCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by7

Results whose statement or proof uses this declaration.