Theorems · Theorem · order theory

List.toFinset_sort

∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r] [inst_4 : DecidableEq α] {l : List α}, l.Nodup → (l.toFinset.sort r = l ↔ List.Pairwise r l)

Defined in

Mathlib.Data.Finset.Sort

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableRelIsTransStd.AntisymmStd.TotalDecidableEq