mathlib3 documentation

algebra.order.interval

Interval arithmetic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines arithmetic operations on intervals and prove their correctness. Note that this is full precision operations. The essentials of float operations can be found in data.fp.basic. We have not yet integrated these with the rest of the library.

One/zero #

source
@[protected, instance]
def nonempty_interval.has_zero {α : Type u_2} [preorder α] [has_zero α] :
has_zero (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.has_one {α : Type u_2} [preorder α] [has_one α] :
has_one (nonempty_interval α)
Equations
source
@[protected, instance]
def interval.has_one {α : Type u_2} [preorder α] [has_one α] :
has_one (interval α)
Equations
source
@[protected, instance]
def interval.has_zero {α : Type u_2} [preorder α] [has_zero α] :
has_zero (interval α)
Equations
source
@[simp]
theorem nonempty_interval.to_prod_one {α : Type u_2} [preorder α] [has_one α] :
1.to_prod = 1
source
@[simp]
theorem nonempty_interval.to_prod_zero {α : Type u_2} [preorder α] [has_zero α] :
0.to_prod = 0
source
theorem nonempty_interval.fst_one {α : Type u_2} [preorder α] [has_one α] :
1.to_prod.fst = 1
source
theorem nonempty_interval.fst_zero {α : Type u_2} [preorder α] [has_zero α] :
0.to_prod.fst = 0
source
theorem nonempty_interval.snd_zero {α : Type u_2} [preorder α] [has_zero α] :
0.to_prod.snd = 0
source
theorem nonempty_interval.snd_one {α : Type u_2} [preorder α] [has_one α] :
1.to_prod.snd = 1
source
@[simp, norm_cast]
theorem nonempty_interval.coe_one_interval {α : Type u_2} [preorder α] [has_one α] :
↑1 = 1
source
@[simp, norm_cast]
theorem nonempty_interval.coe_zero_interval {α : Type u_2} [preorder α] [has_zero α] :
↑0 = 0
source
@[simp]
theorem nonempty_interval.pure_one {α : Type u_2} [preorder α] [has_one α] :
nonempty_interval.pure 1 = 1
source
@[simp]
theorem nonempty_interval.pure_zero {α : Type u_2} [preorder α] [has_zero α] :
nonempty_interval.pure 0 = 0
source
@[simp]
theorem interval.pure_zero {α : Type u_2} [preorder α] [has_zero α] :
interval.pure 0 = 0
source
@[simp]
theorem interval.pure_one {α : Type u_2} [preorder α] [has_one α] :
interval.pure 1 = 1
source
@[simp]
theorem interval.zero_ne_bot {α : Type u_2} [preorder α] [has_zero α] :
0 ≠ ⊥
source
@[simp]
theorem interval.one_ne_bot {α : Type u_2} [preorder α] [has_one α] :
1 ≠ ⊥
source
@[simp]
theorem interval.bot_ne_one {α : Type u_2} [preorder α] [has_one α] :
⊥ ≠ 1
source
@[simp]
theorem interval.bot_ne_zero {α : Type u_2} [preorder α] [has_zero α] :
⊥ ≠ 0
source
@[simp]
theorem nonempty_interval.coe_one {α : Type u_2} [partial_order α] [has_one α] :
↑1 = 1
source
@[simp]
theorem nonempty_interval.coe_zero {α : Type u_2} [partial_order α] [has_zero α] :
↑0 = 0
source
theorem nonempty_interval.zero_mem_zero {α : Type u_2} [partial_order α] [has_zero α] :
0 ∈ 0
source
theorem nonempty_interval.one_mem_one {α : Type u_2} [partial_order α] [has_one α] :
1 ∈ 1
source
@[simp]
theorem interval.coe_one {α : Type u_2} [partial_order α] [has_one α] :
↑1 = 1
source
@[simp]
theorem interval.coe_zero {α : Type u_2} [partial_order α] [has_zero α] :
↑0 = 0
source
theorem interval.one_mem_one {α : Type u_2} [partial_order α] [has_one α] :
1 ∈ 1
source
theorem interval.zero_mem_zero {α : Type u_2} [partial_order α] [has_zero α] :
0 ∈ 0

Addition/multiplication #

Note that this multiplication does not apply to ℚ or ℝ.

source
@[protected, instance]
def nonempty_interval.has_add {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] :
has_add (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.has_mul {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] :
has_mul (nonempty_interval α)
Equations
source
@[protected, instance]
def interval.has_add {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] :
has_add (interval α)
Equations
source
@[protected, instance]
def interval.has_mul {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] :
has_mul (interval α)
Equations
source
@[simp]
theorem nonempty_interval.to_prod_add {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s t : nonempty_interval α) :
(s + t).to_prod = s.to_prod + t.to_prod
source
@[simp]
theorem nonempty_interval.to_prod_mul {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s t : nonempty_interval α) :
(s * t).to_prod = s.to_prod * t.to_prod
source
theorem nonempty_interval.fst_add {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s t : nonempty_interval α) :
(s + t).to_prod.fst = s.to_prod.fst + t.to_prod.fst
source
theorem nonempty_interval.fst_mul {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s t : nonempty_interval α) :
(s * t).to_prod.fst = s.to_prod.fst * t.to_prod.fst
source
theorem nonempty_interval.snd_mul {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s t : nonempty_interval α) :
(s * t).to_prod.snd = s.to_prod.snd * t.to_prod.snd
source
theorem nonempty_interval.snd_add {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s t : nonempty_interval α) :
(s + t).to_prod.snd = s.to_prod.snd + t.to_prod.snd
source
@[simp]
theorem nonempty_interval.coe_add_interval {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s t : nonempty_interval α) :
↑(s + t) = ↑s + ↑t
source
@[simp]
theorem nonempty_interval.coe_mul_interval {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s t : nonempty_interval α) :
↑(s * t) = ↑s * ↑t
source
@[simp]
theorem nonempty_interval.pure_add_pure {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a b : α) :
nonempty_interval.pure a + nonempty_interval.pure b = nonempty_interval.pure (a + b)
source
@[simp]
theorem nonempty_interval.pure_mul_pure {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b : α) :
nonempty_interval.pure a * nonempty_interval.pure b = nonempty_interval.pure (a * b)
source
@[simp]
theorem interval.bot_mul {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (t : interval α) :
⊥ * t = ⊥
source
@[simp]
theorem interval.bot_add {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (t : interval α) :
⊥ + t = ⊥
source
@[simp]
theorem interval.mul_bot {α : Type u_2} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s : interval α) :
s * ⊥ = ⊥
source
@[simp]
theorem interval.add_bot {α : Type u_2} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s : interval α) :
s + ⊥ = ⊥

Powers #

source
@[protected, instance]
def nonempty_interval.has_nsmul {α : Type u_2} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] :
has_smul ℕ (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.has_pow {α : Type u_2} [monoid α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] :
has_pow (nonempty_interval α) ℕ
Equations
source
@[simp]
theorem nonempty_interval.to_prod_pow {α : Type u_2} [monoid α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s : nonempty_interval α) (n : ℕ) :
(s ^ n).to_prod = s.to_prod ^ n
source
@[simp]
theorem nonempty_interval.to_prod_nsmul {α : Type u_2} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s : nonempty_interval α) (n : ℕ) :
(n • s).to_prod = n • s.to_prod
source
theorem nonempty_interval.fst_pow {α : Type u_2} [monoid α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s : nonempty_interval α) (n : ℕ) :
(s ^ n).to_prod.fst = s.to_prod.fst ^ n
source
theorem nonempty_interval.fst_nsmul {α : Type u_2} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s : nonempty_interval α) (n : ℕ) :
(n • s).to_prod.fst = n • s.to_prod.fst
source
theorem nonempty_interval.snd_nsmul {α : Type u_2} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (s : nonempty_interval α) (n : ℕ) :
(n • s).to_prod.snd = n • s.to_prod.snd
source
theorem nonempty_interval.snd_pow {α : Type u_2} [monoid α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (s : nonempty_interval α) (n : ℕ) :
(s ^ n).to_prod.snd = s.to_prod.snd ^ n
source
@[simp]
theorem nonempty_interval.pure_pow {α : Type u_2} [monoid α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) (n : ℕ) :
nonempty_interval.pure a ^ n = nonempty_interval.pure (a ^ n)
source
@[simp]
theorem nonempty_interval.pure_nsmul {α : Type u_2} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) (n : ℕ) :
n • nonempty_interval.pure a = nonempty_interval.pure (n • a)
source
@[protected, instance]
def nonempty_interval.comm_monoid {α : Type u_2} [ordered_comm_monoid α] :
comm_monoid (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.add_comm_monoid {α : Type u_2} [ordered_add_comm_monoid α] :
add_comm_monoid (nonempty_interval α)
Equations
source
@[protected, instance]
def interval.add_zero_class {α : Type u_2} [ordered_add_comm_monoid α] :
add_zero_class (interval α)
Equations
source
@[protected, instance]
def interval.mul_one_class {α : Type u_2} [ordered_comm_monoid α] :
mul_one_class (interval α)
Equations
source
@[protected, instance]
def interval.comm_monoid {α : Type u_2} [ordered_comm_monoid α] :
comm_monoid (interval α)
Equations
source
@[protected, instance]
def interval.add_comm_monoid {α : Type u_2} [ordered_add_comm_monoid α] :
add_comm_monoid (interval α)
Equations
source
@[simp]
theorem nonempty_interval.coe_nsmul_interval {α : Type u_2} [ordered_add_comm_monoid α] (s : nonempty_interval α) (n : ℕ) :
↑(n • s) = n • ↑s
source
@[simp]
theorem nonempty_interval.coe_pow_interval {α : Type u_2} [ordered_comm_monoid α] (s : nonempty_interval α) (n : ℕ) :
↑(s ^ n) = ↑s ^ n
source
theorem interval.bot_pow {α : Type u_2} [ordered_comm_monoid α] {n : ℕ} (hn : n ≠ 0) :
⊥ ^ n = ⊥
source
theorem interval.bot_nsmul {α : Type u_2} [ordered_add_comm_monoid α] {n : ℕ} (hn : n ≠ 0) :
n • ⊥ = ⊥

Subtraction #

Subtraction is defined more generally than division so that it applies to ℕ (and has_ordered_div is not a thing and probably should not become one).

source
@[protected, instance]
def nonempty_interval.has_sub {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] :
has_sub (nonempty_interval α)
Equations
source
@[protected, instance]
def interval.has_sub {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] :
has_sub (interval α)
Equations
source
@[simp]
theorem nonempty_interval.fst_sub {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (s t : nonempty_interval α) :
(s - t).to_prod.fst = s.to_prod.fst - t.to_prod.snd
source
@[simp]
theorem nonempty_interval.snd_sub {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (s t : nonempty_interval α) :
(s - t).to_prod.snd = s.to_prod.snd - t.to_prod.fst
source
@[simp]
theorem nonempty_interval.coe_sub_interval {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (s t : nonempty_interval α) :
↑(s - t) = ↑s - ↑t
source
theorem nonempty_interval.sub_mem_sub {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (s t : nonempty_interval α) {a b : α} (ha : a ∈ s) (hb : b ∈ t) :
a - b ∈ s - t
source
@[simp]
theorem nonempty_interval.pure_sub_pure {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (a b : α) :
nonempty_interval.pure a - nonempty_interval.pure b = nonempty_interval.pure (a - b)
source
@[simp]
theorem interval.bot_sub {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (t : interval α) :
⊥ - t = ⊥
source
@[simp]
theorem interval.sub_bot {α : Type u_2} [preorder α] [add_comm_semigroup α] [has_sub α] [has_ordered_sub α] [covariant_class α α has_add.add has_le.le] (s : interval α) :
s - ⊥ = ⊥

Division in ordered groups #

Note that this division does not apply to ℚ or ℝ.

source
@[protected, instance]
def nonempty_interval.has_div {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] :
has_div (nonempty_interval α)
Equations
source
@[protected, instance]
def interval.has_div {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] :
has_div (interval α)
Equations
source
@[simp]
theorem nonempty_interval.fst_div {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (s t : nonempty_interval α) :
(s / t).to_prod.fst = s.to_prod.fst / t.to_prod.snd
source
@[simp]
theorem nonempty_interval.snd_div {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (s t : nonempty_interval α) :
(s / t).to_prod.snd = s.to_prod.snd / t.to_prod.fst
source
@[simp]
theorem nonempty_interval.coe_div_interval {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (s t : nonempty_interval α) :
↑(s / t) = ↑s / ↑t
source
theorem nonempty_interval.div_mem_div {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (s t : nonempty_interval α) (a b : α) (ha : a ∈ s) (hb : b ∈ t) :
a / b ∈ s / t
source
@[simp]
theorem nonempty_interval.pure_div_pure {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (a b : α) :
nonempty_interval.pure a / nonempty_interval.pure b = nonempty_interval.pure (a / b)
source
@[simp]
theorem interval.bot_div {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (t : interval α) :
⊥ / t = ⊥
source
@[simp]
theorem interval.div_bot {α : Type u_2} [preorder α] [comm_group α] [covariant_class α α has_mul.mul has_le.le] (s : interval α) :
s / ⊥ = ⊥

Negation/inversion #

source
@[protected, instance]
def nonempty_interval.has_inv {α : Type u_2} [ordered_comm_group α] :
has_inv (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.has_neg {α : Type u_2} [ordered_add_comm_group α] :
has_neg (nonempty_interval α)
Equations
source
@[protected, instance]
def interval.has_neg {α : Type u_2} [ordered_add_comm_group α] :
has_neg (interval α)
Equations
source
@[protected, instance]
def interval.has_inv {α : Type u_2} [ordered_comm_group α] :
has_inv (interval α)
Equations
source
@[simp]
theorem nonempty_interval.fst_inv {α : Type u_2} [ordered_comm_group α] (s : nonempty_interval α) :
s⁻¹.to_prod.fst = (s.to_prod.snd)⁻¹
source
@[simp]
theorem nonempty_interval.fst_neg {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) :
(-s).to_prod.fst = -s.to_prod.snd
source
@[simp]
theorem nonempty_interval.snd_neg {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) :
(-s).to_prod.snd = -s.to_prod.fst
source
@[simp]
theorem nonempty_interval.snd_inv {α : Type u_2} [ordered_comm_group α] (s : nonempty_interval α) :
s⁻¹.to_prod.snd = (s.to_prod.fst)⁻¹
source
@[simp]
theorem nonempty_interval.coe_inv_interval {α : Type u_2} [ordered_comm_group α] (s : nonempty_interval α) :
↑s⁻¹ = (↑s)⁻¹
source
@[simp]
theorem nonempty_interval.coe_neg_interval {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) :
↑-s = -↑s
source
theorem nonempty_interval.inv_mem_inv {α : Type u_2} [ordered_comm_group α] (s : nonempty_interval α) (a : α) (ha : a ∈ s) :
a⁻¹ ∈ s⁻¹
source
theorem nonempty_interval.neg_mem_neg {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) (a : α) (ha : a ∈ s) :
-a ∈ -s
source
@[simp]
theorem nonempty_interval.inv_pure {α : Type u_2} [ordered_comm_group α] (a : α) :
(nonempty_interval.pure a)⁻¹ = nonempty_interval.pure a⁻¹
source
@[simp]
theorem nonempty_interval.neg_pure {α : Type u_2} [ordered_add_comm_group α] (a : α) :
-nonempty_interval.pure a = nonempty_interval.pure (-a)
source
@[simp]
theorem interval.inv_bot {α : Type u_2} [ordered_comm_group α] :
⊥⁻¹ = ⊥
source
@[simp]
theorem interval.neg_bot {α : Type u_2} [ordered_add_comm_group α] :
-⊥ = ⊥
source
@[protected]
theorem nonempty_interval.mul_eq_one_iff {α : Type u_2} [ordered_comm_group α] {s t : nonempty_interval α} :
s * t = 1 ↔ ∃ (a b : α), s = nonempty_interval.pure a ∧ t = nonempty_interval.pure b ∧ a * b = 1
source
@[protected]
theorem nonempty_interval.add_eq_zero_iff {α : Type u_2} [ordered_add_comm_group α] {s t : nonempty_interval α} :
s + t = 0 ↔ ∃ (a b : α), s = nonempty_interval.pure a ∧ t = nonempty_interval.pure b ∧ a + b = 0
source
@[protected, instance]
def nonempty_interval.subtraction_comm_monoid {α : Type u} [ordered_add_comm_group α] :
subtraction_comm_monoid (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.division_comm_monoid {α : Type u_2} [ordered_comm_group α] :
division_comm_monoid (nonempty_interval α)
Equations
source
@[protected]
theorem interval.add_eq_zero_iff {α : Type u_2} [ordered_add_comm_group α] {s t : interval α} :
s + t = 0 ↔ ∃ (a b : α), s = interval.pure a ∧ t = interval.pure b ∧ a + b = 0
source
@[protected]
theorem interval.mul_eq_one_iff {α : Type u_2} [ordered_comm_group α] {s t : interval α} :
s * t = 1 ↔ ∃ (a b : α), s = interval.pure a ∧ t = interval.pure b ∧ a * b = 1
source
@[protected, instance]
def interval.subtraction_comm_monoid {α : Type u} [ordered_add_comm_group α] :
subtraction_comm_monoid (interval α)
Equations
source
@[protected, instance]
def interval.division_comm_monoid {α : Type u_2} [ordered_comm_group α] :
division_comm_monoid (interval α)
Equations
source
def nonempty_interval.length {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) :
α

The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval.

Equations
source
@[simp]
theorem nonempty_interval.length_nonneg {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) :
0 ≤ s.length
source
@[simp]
theorem nonempty_interval.length_pure {α : Type u_2} [ordered_add_comm_group α] (a : α) :
(nonempty_interval.pure a).length = 0
source
@[simp]
theorem nonempty_interval.length_zero {α : Type u_2} [ordered_add_comm_group α] :
0.length = 0
source
@[simp]
theorem nonempty_interval.length_neg {α : Type u_2} [ordered_add_comm_group α] (s : nonempty_interval α) :
(-s).length = s.length
source
@[simp]
theorem nonempty_interval.length_add {α : Type u_2} [ordered_add_comm_group α] (s t : nonempty_interval α) :
(s + t).length = s.length + t.length
source
@[simp]
theorem nonempty_interval.length_sub {α : Type u_2} [ordered_add_comm_group α] (s t : nonempty_interval α) :
(s - t).length = s.length + t.length
source
@[simp]
theorem nonempty_interval.length_sum {ι : Type u_1} {α : Type u_2} [ordered_add_comm_group α] (f : ι → nonempty_interval α) (s : finset ι) :
(s.sum (λ (i : ι), f i)).length = s.sum (λ (i : ι), (f i).length)
source
def interval.length {α : Type u_2} [ordered_add_comm_group α] :
interval α → α

The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval.

Equations
source
@[simp]
theorem interval.length_nonneg {α : Type u_2} [ordered_add_comm_group α] (s : interval α) :
0 ≤ s.length
source
@[simp]
theorem interval.length_pure {α : Type u_2} [ordered_add_comm_group α] (a : α) :
(interval.pure a).length = 0
source
@[simp]
theorem interval.length_zero {α : Type u_2} [ordered_add_comm_group α] :
0.length = 0
source
@[simp]
theorem interval.length_neg {α : Type u_2} [ordered_add_comm_group α] (s : interval α) :
(-s).length = s.length
source
theorem interval.length_add_le {α : Type u_2} [ordered_add_comm_group α] (s t : interval α) :
(s + t).length ≤ s.length + t.length
source
theorem interval.length_sub_le {α : Type u_2} [ordered_add_comm_group α] (s t : interval α) :
(s - t).length ≤ s.length + t.length
source
theorem interval.length_sum_le {ι : Type u_1} {α : Type u_2} [ordered_add_comm_group α] (f : ι → interval α) (s : finset ι) :
(s.sum (λ (i : ι), f i)).length ≤ s.sum (λ (i : ι), (f i).length)
source
meta def tactic.positivity_interval_length  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: The length of an interval is always nonnegative.