Commit 2022-11-30 19:51 1a513788

View on Github →

feat(algebra/order/interval): Interval arithmetic (#16761) Define arithmetic operations on interval/nonempty_interval and prove their correctness.

Estimated changes

Created src/algebra/order/interval.lean

added theorem interval.bot_div

added theorem interval.bot_mul

added theorem interval.bot_ne_one

added theorem interval.bot_pow

added theorem interval.bot_sub

added theorem interval.coe_one

added theorem interval.div_bot

added theorem interval.inv_bot

added def interval.length

added theorem interval.length_add_le

added theorem interval.length_neg

added theorem interval.length_nonneg

added theorem interval.length_pure

added theorem interval.length_sub_le

added theorem interval.length_sum_le

added theorem interval.length_zero

added theorem interval.mul_bot

added theorem interval.one_mem_one

added theorem interval.one_ne_bot

added theorem interval.pure_one

added theorem interval.sub_bot

added theorem nonempty_interval.coe_div_interval

added theorem nonempty_interval.coe_inv_interval

added theorem nonempty_interval.coe_mul_interval

added theorem nonempty_interval.coe_one

added theorem nonempty_interval.coe_one_interval

added theorem nonempty_interval.coe_pow_interval

added theorem nonempty_interval.coe_sub_interval

added theorem nonempty_interval.div_mem_div

added theorem nonempty_interval.fst_div

added theorem nonempty_interval.fst_inv

added theorem nonempty_interval.fst_mul

added theorem nonempty_interval.fst_one

added theorem nonempty_interval.fst_pow

added theorem nonempty_interval.fst_sub

added theorem nonempty_interval.inv_mem_inv

added theorem nonempty_interval.inv_pure

added def nonempty_interval.length

added theorem nonempty_interval.length_add

added theorem nonempty_interval.length_neg

added theorem nonempty_interval.length_nonneg

added theorem nonempty_interval.length_pure

added theorem nonempty_interval.length_sub

added theorem nonempty_interval.length_sum

added theorem nonempty_interval.length_zero

added theorem nonempty_interval.one_mem_one

added theorem nonempty_interval.pure_div_pure

added theorem nonempty_interval.pure_mul_pure

added theorem nonempty_interval.pure_one

added theorem nonempty_interval.pure_pow

added theorem nonempty_interval.pure_sub_pure

added theorem nonempty_interval.snd_div

added theorem nonempty_interval.snd_inv

added theorem nonempty_interval.snd_mul

added theorem nonempty_interval.snd_one

added theorem nonempty_interval.snd_pow

added theorem nonempty_interval.snd_sub

added theorem nonempty_interval.sub_mem_sub

added theorem nonempty_interval.to_prod_mul

added theorem nonempty_interval.to_prod_one

added theorem nonempty_interval.to_prod_pow

Modified src/algebra/order/monoid/lemmas.lean

added theorem mul_le_mul_iff_of_ge

Modified src/order/interval.lean

added theorem interval.bot_ne_pure

added theorem interval.mem_pure

added theorem interval.mem_pure_self

added theorem interval.pure_ne_bot

added theorem interval.subset_coe_map

added theorem nonempty_interval.coe_eq_pure

modified theorem nonempty_interval.coe_pure

modified theorem nonempty_interval.coe_pure_interval

added theorem nonempty_interval.dual_map₂

added def nonempty_interval.map₂

added theorem nonempty_interval.map₂_pure

added theorem nonempty_interval.mem_pure

added theorem nonempty_interval.mem_pure_self

added theorem nonempty_interval.subset_coe_map

added theorem nonempty_interval.to_prod_injective

Modified test/positivity.lean