Theorem Tuple.lt_card_le_iff_apply_le_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) …
Modified Tuple.lt_card_le_iff_apply_le_of_monotoneView on Github →
2025-03-17 06:31
Mathlib/Data/Fin/Tuple/Sort.lean
chore: Migrate to `DecidableLT` and `DecidableLE` (#22238) …
Modified Tuple.lt_card_le_iff_apply_le_of_monotoneView on Github →
2025-03-05 06:23
Mathlib/Data/Fin/Tuple/Sort.lean
feat: generalize order typeclasses (#22569) …
Modified Tuple.lt_card_le_iff_apply_le_of_monotoneView on Github →
2023-09-02 20:42
Mathlib/Data/Fin/Tuple/Sort.lean
feat: Elements less than some value of a sorted tuple are at the beginning of the tuple. (#6728) …
Added Tuple.lt_card_le_iff_apply_le_of_monotoneView on Github →