Commit 2020-09-30 09:51 e53aa870

View on Github →

feat(order/basic): lemmas about strict_mono_incr_on (#4313) Also move the section about order_dual up to use it in the proofs. Non-BC API changes:

Now strict_mono_incr_on and strict_mono_decr_on take x and y as ⦃⦄ args.

Estimated changes

Modified archive/100-theorems-list/73_ascending_descending_sequences.lean

Modified src/data/set/function.lean

added theorem strict_mono_decr_on.inj_on

added theorem strict_mono_incr_on.inj_on

Modified src/order/basic.lean

added theorem order_dual.dual_compares

deleted theorem strict_mono.compares

modified theorem strict_mono.injective

modified theorem strict_mono.le_iff_le

modified theorem strict_mono.lt_iff_lt

added theorem strict_mono_decr_on.le_iff_le

added theorem strict_mono_decr_on.lt_iff_lt

added theorem strict_mono_incr_on.le_iff_le

added theorem strict_mono_incr_on.lt_iff_lt

added theorem subtype.coe_le_coe

added theorem subtype.coe_lt_coe

added theorem subtype.mk_le_mk

added theorem subtype.mk_lt_mk

Modified src/order/rel_iso.lean

added theorem order_iso.coe_to_order_embedding

added def order_iso.to_order_embedding