Mathlib Changelog
v4
Changelog
About
Github
Theorem
Tuple.lt_card_gt_iff_apply_gt_of_antitone
Modification history
2026-01-26 23:09
Mathlib/Data/Fin/Tuple/Sort.lean
chore(Data/Fin/Tuple/Sort): generalise and golf `lt_card` lemmas (#34353) …
Added
Tuple.lt_card_gt_iff_apply_gt_of_antitone
View on Github →