Documentation

Mathlib.Algebra.Order.Interval.Basic

Interval arithmetic #

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 #

instance instZeroNonemptyInterval {α : Type u_2} [Preorder α] [Zero α] :
Equations
instance instOneNonemptyInterval {α : Type u_2} [Preorder α] [One α] :
Equations
@[simp]
theorem NonemptyInterval.coe_zero_interval {α : Type u_2} [Preorder α] [Zero α] :
0 = 0
@[simp]
theorem NonemptyInterval.coe_one_interval {α : Type u_2} [Preorder α] [One α] :
1 = 1
@[simp]
@[simp]
@[simp]
theorem Interval.pure_zero {α : Type u_2} [Preorder α] [Zero α] :
@[simp]
theorem Interval.pure_one {α : Type u_2} [Preorder α] [One α] :
theorem Interval.zero_ne_bot {α : Type u_2} [Preorder α] [Zero α] :
theorem Interval.one_ne_bot {α : Type u_2} [Preorder α] [One α] :
theorem Interval.bot_ne_zero {α : Type u_2} [Preorder α] [Zero α] :
theorem Interval.bot_ne_one {α : Type u_2} [Preorder α] [One α] :
@[simp]
theorem NonemptyInterval.coe_zero {α : Type u_2} [PartialOrder α] [Zero α] :
0 = 0
@[simp]
theorem NonemptyInterval.coe_one {α : Type u_2} [PartialOrder α] [One α] :
1 = 1
theorem NonemptyInterval.one_mem_one {α : Type u_2} [PartialOrder α] [One α] :
1 1
@[simp]
theorem Interval.coe_zero {α : Type u_2} [PartialOrder α] [Zero α] :
0 = 0
@[simp]
theorem Interval.coe_one {α : Type u_2} [PartialOrder α] [One α] :
1 = 1
theorem Interval.zero_mem_zero {α : Type u_2} [PartialOrder α] [Zero α] :
0 0
theorem Interval.one_mem_one {α : Type u_2} [PartialOrder α] [One α] :
1 1

Addition/multiplication #

Note that this multiplication does not apply to or .

instance instAddNonemptyInterval {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • instAddNonemptyInterval = { add := fun (s t : NonemptyInterval α) => { toProd := s.toProd + t.toProd, fst_le_snd := } }
theorem instAddNonemptyInterval.proof_1 {α : Type u_1} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
s.toProd.1 + t.toProd.1 s.toProd.2 + t.toProd.2
instance instMulNonemptyInterval {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • instMulNonemptyInterval = { mul := fun (s t : NonemptyInterval α) => { toProd := s.toProd * t.toProd, fst_le_snd := } }
instance instAddInterval {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
Equations
instance instMulInterval {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
Equations
@[simp]
theorem NonemptyInterval.toProd_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s + t).toProd = s.toProd + t.toProd
@[simp]
theorem NonemptyInterval.toProd_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s * t).toProd = s.toProd * t.toProd
theorem NonemptyInterval.fst_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s + t).toProd.1 = s.toProd.1 + t.toProd.1
theorem NonemptyInterval.fst_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s * t).toProd.1 = s.toProd.1 * t.toProd.1
theorem NonemptyInterval.snd_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s + t).toProd.2 = s.toProd.2 + t.toProd.2
theorem NonemptyInterval.snd_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s * t).toProd.2 = s.toProd.2 * t.toProd.2
@[simp]
theorem NonemptyInterval.coe_add_interval {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s + t) = s + t
@[simp]
theorem NonemptyInterval.coe_mul_interval {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s * t) = s * t
@[simp]
theorem NonemptyInterval.pure_add_pure {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
@[simp]
theorem NonemptyInterval.pure_mul_pure {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
@[simp]
theorem Interval.bot_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (t : Interval α) :
@[simp]
theorem Interval.bot_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (t : Interval α) :
theorem Interval.add_bot {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : Interval α) :
@[simp]
theorem Interval.mul_bot {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : Interval α) :

Powers #

instance NonemptyInterval.hasNSMul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • NonemptyInterval.hasNSMul = { smul := fun (n : ) (s : NonemptyInterval α) => { toProd := (n s.toProd.1, n s.toProd.2), fst_le_snd := } }
instance NonemptyInterval.hasPow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • NonemptyInterval.hasPow = { pow := fun (s : NonemptyInterval α) (n : ) => { toProd := s.toProd ^ n, fst_le_snd := } }
@[simp]
theorem NonemptyInterval.toProd_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (n : ) :
(n s).toProd = n s.toProd
@[simp]
theorem NonemptyInterval.toProd_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (n : ) :
(s ^ n).toProd = s.toProd ^ n
theorem NonemptyInterval.fst_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (n : ) :
(n s).toProd.1 = n s.toProd.1
theorem NonemptyInterval.fst_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (n : ) :
(s ^ n).toProd.1 = s.toProd.1 ^ n
theorem NonemptyInterval.snd_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (n : ) :
(n s).toProd.2 = n s.toProd.2
theorem NonemptyInterval.snd_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (n : ) :
(s ^ n).toProd.2 = s.toProd.2 ^ n
@[simp]
theorem NonemptyInterval.pure_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (n : ) :
@[simp]
theorem NonemptyInterval.pure_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (n : ) :
Equations
theorem NonemptyInterval.addCommMonoid.proof_6 {α : Type u_1} [OrderedAddCommMonoid α] (s : NonemptyInterval α) (n : ) :
(n s).toProd = n s.toProd
theorem NonemptyInterval.addCommMonoid.proof_2 {α : Type u_1} [OrderedAddCommMonoid α] :
CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2
theorem NonemptyInterval.addCommMonoid.proof_5 {α : Type u_1} [OrderedAddCommMonoid α] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s + t).toProd = s.toProd + t.toProd
theorem NonemptyInterval.addCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] :
CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2
Equations
theorem Interval.addZeroClass.proof_2 {α : Type u_1} [OrderedAddCommMonoid α] (s : Interval α) :
Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) (some 0) s = s
theorem Interval.addZeroClass.proof_3 {α : Type u_1} [OrderedAddCommMonoid α] (s : Interval α) :
Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) s (some 0) = s
Equations
theorem Interval.addZeroClass.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] :
CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2
Equations
theorem Interval.addCommMonoid.proof_4 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (x : Interval α), nsmulRec 0 x = nsmulRec 0 x
theorem Interval.addCommMonoid.proof_5 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (n : ) (x : Interval α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
Equations
theorem Interval.addCommMonoid.proof_6 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (x x_1 : Interval α), Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) x x_1 = Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) x_1 x
theorem Interval.addCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (x x_1 x_2 : Interval α), Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) (Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) x x_1) x_2 = Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) x (Option.map₂ (fun (x1 x2 : NonemptyInterval α) => x1 + x2) x_1 x_2)
Equations
theorem NonemptyInterval.coe_nsmul_interval {α : Type u_2} [OrderedAddCommMonoid α] (s : NonemptyInterval α) (n : ) :
(n s) = n s
@[simp]
theorem NonemptyInterval.coe_pow_interval {α : Type u_2} [OrderedCommMonoid α] (s : NonemptyInterval α) (n : ) :
(s ^ n) = s ^ n
theorem Interval.bot_nsmul {α : Type u_2} [OrderedAddCommMonoid α] {n : } :
n 0n =
theorem Interval.bot_pow {α : Type u_2} [OrderedCommMonoid α] {n : } :
n 0 ^ n =

Subtraction #

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

instance instSubNonemptyInterval {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • instSubNonemptyInterval = { sub := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 - t.toProd.2, s.toProd.2 - t.toProd.1), fst_le_snd := } }
instance instSubInterval {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
Equations
@[simp]
theorem NonemptyInterval.fst_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s - t).toProd.1 = s.toProd.1 - t.toProd.2
@[simp]
theorem NonemptyInterval.snd_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s - t).toProd.2 = s.toProd.2 - t.toProd.1
@[simp]
theorem NonemptyInterval.coe_sub_interval {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s - t) = s - t
theorem NonemptyInterval.sub_mem_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) {a : α} {b : α} (ha : a s) (hb : b t) :
a - b s - t
@[simp]
theorem NonemptyInterval.pure_sub_pure {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
@[simp]
theorem Interval.bot_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (t : Interval α) :
@[simp]
theorem Interval.sub_bot {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (s : Interval α) :

Division in ordered groups #

Note that this division does not apply to or .

instance instDivNonemptyInterval {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
Equations
  • instDivNonemptyInterval = { div := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 / t.toProd.2, s.toProd.2 / t.toProd.1), fst_le_snd := } }
instance instDivInterval {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
Equations
@[simp]
theorem NonemptyInterval.fst_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s / t).toProd.1 = s.toProd.1 / t.toProd.2
@[simp]
theorem NonemptyInterval.snd_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s / t).toProd.2 = s.toProd.2 / t.toProd.1
@[simp]
theorem NonemptyInterval.coe_div_interval {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) :
(s / t) = s / t
theorem NonemptyInterval.div_mem_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : NonemptyInterval α) (t : NonemptyInterval α) (a : α) (b : α) (ha : a s) (hb : b t) :
a / b s / t
@[simp]
theorem NonemptyInterval.pure_div_pure {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
@[simp]
theorem Interval.bot_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (t : Interval α) :
@[simp]
theorem Interval.div_bot {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (s : Interval α) :

Negation/inversion #

theorem instNegNonemptyInterval.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : NonemptyInterval α) :
-s.toProd.2 -s.toProd.1
Equations
  • instNegNonemptyInterval = { neg := fun (s : NonemptyInterval α) => { toProd := (-s.toProd.2, -s.toProd.1), fst_le_snd := } }
Equations
  • instInvNonemptyInterval = { inv := fun (s : NonemptyInterval α) => { toProd := (s.toProd.2⁻¹, s.toProd.1⁻¹), fst_le_snd := } }
instance instNegInterval {α : Type u_2} [OrderedAddCommGroup α] :
Equations
instance instInvInterval {α : Type u_2} [OrderedCommGroup α] :
Equations
@[simp]
theorem NonemptyInterval.fst_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) :
(-s).toProd.1 = -s.toProd.2
@[simp]
theorem NonemptyInterval.fst_inv {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) :
s⁻¹.toProd.1 = s.toProd.2⁻¹
@[simp]
theorem NonemptyInterval.snd_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) :
(-s).toProd.2 = -s.toProd.1
@[simp]
theorem NonemptyInterval.snd_inv {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) :
s⁻¹.toProd.2 = s.toProd.1⁻¹
@[simp]
theorem NonemptyInterval.coe_neg_interval {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) :
(-s) = -s
@[simp]
theorem NonemptyInterval.neg_mem_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) (a : α) (ha : a s) :
-a -s
theorem NonemptyInterval.inv_mem_inv {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) (a : α) (ha : a s) :
@[simp]
@[simp]
theorem NonemptyInterval.add_eq_zero_iff {α : Type u_2} [OrderedAddCommGroup α] {s : NonemptyInterval α} {t : NonemptyInterval α} :
s + t = 0 ∃ (a : α) (b : α), s = NonemptyInterval.pure a t = NonemptyInterval.pure b a + b = 0
theorem NonemptyInterval.mul_eq_one_iff {α : Type u_2} [OrderedCommGroup α] {s : NonemptyInterval α} {t : NonemptyInterval α} :
s * t = 1 ∃ (a : α) (b : α), s = NonemptyInterval.pure a t = NonemptyInterval.pure b a * b = 1
Equations
Equations
theorem Interval.add_eq_zero_iff {α : Type u_2} [OrderedAddCommGroup α] {s : Interval α} {t : Interval α} :
s + t = 0 ∃ (a : α) (b : α), s = Interval.pure a t = Interval.pure b a + b = 0
theorem Interval.mul_eq_one_iff {α : Type u_2} [OrderedCommGroup α] {s : Interval α} {t : Interval α} :
s * t = 1 ∃ (a : α) (b : α), s = Interval.pure a t = Interval.pure b a * b = 1
Equations
Equations

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

Equations
  • s.length = s.toProd.2 - s.toProd.1
Instances For
    @[simp]
    theorem NonemptyInterval.length_nonneg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) :
    0 s.length
    @[simp]
    theorem NonemptyInterval.length_pure {α : Type u_2} [OrderedAddCommGroup α] (a : α) :
    @[simp]
    theorem NonemptyInterval.length_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) :
    (-s).length = s.length
    @[simp]
    theorem NonemptyInterval.length_add {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) (t : NonemptyInterval α) :
    (s + t).length = s.length + t.length
    @[simp]
    theorem NonemptyInterval.length_sub {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) (t : NonemptyInterval α) :
    (s - t).length = s.length + t.length
    @[simp]
    theorem NonemptyInterval.length_sum {ι : Type u_1} {α : Type u_2} [OrderedAddCommGroup α] (f : ιNonemptyInterval α) (s : Finset ι) :
    (∑ is, f i).length = is, (f i).length
    def Interval.length {α : Type u_2} [OrderedAddCommGroup α] :
    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
    Instances For
      @[simp]
      theorem Interval.length_nonneg {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) :
      0 s.length
      @[simp]
      theorem Interval.length_pure {α : Type u_2} [OrderedAddCommGroup α] (a : α) :
      (Interval.pure a).length = 0
      @[simp]
      theorem Interval.length_neg {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) :
      (-s).length = s.length
      theorem Interval.length_add_le {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) (t : Interval α) :
      (s + t).length s.length + t.length
      theorem Interval.length_sub_le {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) (t : Interval α) :
      (s - t).length s.length + t.length
      theorem Interval.length_sum_le {ι : Type u_1} {α : Type u_2} [OrderedAddCommGroup α] (f : ιInterval α) (s : Finset ι) :
      (∑ is, f i).length is, (f i).length

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

      Instances For

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

        Instances For