Mathlib Map

Theorems · Theorem · order theory

Finset.sort.congr_simp

∀ {α : Type u_1} (s s_1 : Finset α),
  s = s_1 →
    ∀ (r r_1 : α → α → Prop) (e_r : r = r_1) {inst : DecidableRel r} [inst_1 : DecidableRel r_1] [inst_2 : IsTrans α r]
      [inst_3 : Std.Antisymm r] [inst_4 : Std.Total r], s.sort r = s_1.sort r_1
Defined in
Mathlib.Data.Finset.Sort
Cited by
2 results in Mathlib
Foundations
Depth 61 from the axioms · uses propext, Quot.sound
Assumes
DecidableRelIsTransStd.AntisymmStd.Total
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Ordinal.CNF.eval_single_add' · cited by 5CNF.eval_single_add'Ordinal.CNF.eval_zero_right · cited by 5CNF.eval_zero_rightFinset · cited by 13712FinsetIsTrans · cited by 157IsTransFinset.sort · cited by 42Finset.sortsort.congr_simpCITED BYCITES

Cites3

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

  • Finsetstatement and proof · cited by 13,712
  • IsTransstatement and proof · cited by 157
  • Finset.sortstatement and proof · cited by 42

Cited by2

Results whose statement or proof uses this declaration.