Commit 2023-01-25 10:48 fb29af61

View on Github →

feat: port Data.Fin.Tuple.Monotone (#1827)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fin/Tuple/Monotone.lean

added theorem Antitone.vecCons

added theorem Monotone.vecCons

added theorem StrictAnti.vecCons

added theorem StrictMono.vecCons

added theorem antitone_vecCons

added theorem antitone_vecEmpty

added theorem lift_fun_vecCons

added theorem monotone_vecCons

added theorem monotone_vecEmpty

added theorem strictAnti_vecCons

added theorem strictAnti_vecEmpty

added theorem strictMono_vecCons

added theorem strictMono_vecEmpty