Theorems · Theorem · order theory

Finset.sort_cons

∀ {α : Type u_1} {s : Finset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] {a : α},
  (∀ b ∈ s, r a b) → ∀ (h₂ : a ∉ s), (Finset.cons a s h₂).sort r = a :: s.sort r

Defined in

Mathlib.Data.Finset.Sort

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableRelIsTransStd.AntisymmStd.Total