Commit 2026-01-26 23:09 dddace28

View on Github →

chore(Data/Fin/Tuple/Sort): generalise and golf lt_card lemmas (#34353) The statement has a nice generalisation which doesn't use tuples, and allows easy expression of a few useful variants.

Estimated changes

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

modified theorem Tuple.lt_card_ge_iff_apply_ge_of_antitone

added theorem Tuple.lt_card_gt_iff_apply_gt_of_antitone

modified theorem Tuple.lt_card_le_iff_apply_le_of_monotone

added theorem Tuple.lt_card_lt_iff_apply_lt_of_monotone

Modified Mathlib/Data/Fintype/Fin.lean

added theorem Fin.lt_card_filter_univ_iff_apply_of_imp