Commit 2023-06-07 16:52 4eebfa2e

View on Github →

feat: port Algebra.Order.Interval (#4464)

Estimated changes

Modified Mathlib.lean

Created Mathlib/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 def Mathlib.Meta.Positivity.evalIntervalLength

added def Mathlib.Meta.Positivity.evalNonemptyIntervalLength

added theorem NonemptyInterval.coe_div_interval

added theorem NonemptyInterval.coe_inv_interval

added theorem NonemptyInterval.coe_mul_interval

added theorem NonemptyInterval.coe_one

added theorem NonemptyInterval.coe_one_interval

added theorem NonemptyInterval.coe_pow_interval

added theorem NonemptyInterval.coe_sub_interval

added theorem NonemptyInterval.div_mem_div

added theorem NonemptyInterval.fst_div

added theorem NonemptyInterval.fst_inv

added theorem NonemptyInterval.fst_mul

added theorem NonemptyInterval.fst_one

added theorem NonemptyInterval.fst_pow

added theorem NonemptyInterval.fst_sub

added theorem NonemptyInterval.inv_mem_inv

added theorem NonemptyInterval.inv_pure

added def NonemptyInterval.length

added theorem NonemptyInterval.length_add

added theorem NonemptyInterval.length_neg

added theorem NonemptyInterval.length_nonneg

added theorem NonemptyInterval.length_pure

added theorem NonemptyInterval.length_sub

added theorem NonemptyInterval.length_sum

added theorem NonemptyInterval.length_zero

added theorem NonemptyInterval.one_mem_one

added theorem NonemptyInterval.pure_div_pure

added theorem NonemptyInterval.pure_mul_pure

added theorem NonemptyInterval.pure_one

added theorem NonemptyInterval.pure_pow

added theorem NonemptyInterval.pure_sub_pure

added theorem NonemptyInterval.snd_div

added theorem NonemptyInterval.snd_inv

added theorem NonemptyInterval.snd_mul

added theorem NonemptyInterval.snd_one

added theorem NonemptyInterval.snd_pow

added theorem NonemptyInterval.snd_sub

added theorem NonemptyInterval.sub_mem_sub

added theorem NonemptyInterval.toProd_mul

added theorem NonemptyInterval.toProd_one

added theorem NonemptyInterval.toProd_pow