Theorem Tuple.lt_card_lt_iff_apply_lt_of_monotone

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_lt_iff_apply_lt_of_monotoneView on Github →