Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 13:49 f855a4ba

View on Github →

feat(order/monotone): Monotonicity of prod.map (#14843) If f and g are monotone/antitone, then prod.map f g is as well.

Estimated changes

added theorem antitone.imp
added theorem antitone.prod_map
added theorem monotone.imp
added theorem monotone.prod_map
modified theorem monotone_fst
modified theorem monotone_snd
added theorem strict_anti.imp
added theorem strict_anti.prod_map
added theorem strict_mono.imp
added theorem strict_mono.prod_map