Theorems · Theorem · order theory

Finset.sort_singleton

∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r] (a : α), {a}.sort r = [a]

Defined in: Mathlib.Data.Finset.Sort
Cited by: 0 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Quot.sound
Assumes: DecidableRel IsTrans Std.Antisymm Std.Total

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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

Finsetstatement · cited by 13,712
IsTransstatement and proof · cited by 157
Finset.sortstatement · cited by 42
Multiset.sort_singletonproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.