Commit 2025-03-21 09:08 72de784c

View on Github →

chore(Tuple/Sort): dualize unique_monotone to unique_antitone (#23046) From "Formalizing the Bruhat-Tits tree".

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Sort.lean

added theorem Tuple.unique_antitone

Modified Mathlib/Data/List/Sort.lean

added theorem List.sorted_ge_ofFn_iff

added theorem List.sorted_gt_ofFn_iff