(possibly unbounded) intervals

This file defines the Interval type for computation in the inclusion tactic. This type represents a possibly unbounded interval with closed endpoints.

structure Inclusion.Interval (α : Type u_3) : Type u_3

An Interval represents a possibly unbounded interval with closed endpoints.

• lb : WithBot α

  The lower endpoint, or ⊥ if the interval is unbounded below.

• ub : WithTop α

  The upper endpoint, or ⊤ if the interval is unbounded above.

@[instance_reducible]

instance Inclusion.instInhabitedInterval {a✝ : Type u_3} : Inhabited (Interval a✝)

Equations

• Inclusion.instInhabitedInterval = { default := Inclusion.instInhabitedInterval.default }

def Inclusion.Interval.toSet {α : Type u_1} [Preorder α] (I : Interval α) : Set α

Maps I to {a | I.lb ≤ a ∧ a ≤ I.ub}

Equations

• I.toSet = {a : α | I.lb ≤ ↑a ∧ ↑a ≤ I.ub}

@[instance_reducible]

instance Inclusion.instToSetIntervalOfPreorder {α : Type u_1} [Preorder α] : ToSet (Interval α) α

Equations

• Inclusion.instToSetIntervalOfPreorder = { toSet := Inclusion.Interval.toSet }

@[simp]

theorem Inclusion.Interval.mem_def {α : Type u_1} [Preorder α] {x : α} {I : Interval α} : x ∈ I ↔ I.lb ≤ ↑x ∧ ↑x ≤ I.ub

def Inclusion.Interval.map {α : Type u_1} {β : Type u_2} (I : Interval α) (f : α → β) : Interval β

Apply a function to the finite endpoints of an interval.

Equations

• I.map f = { lb := WithBot.map f I.lb, ub := WithTop.map f I.ub }

theorem Inclusion.Interval.mem_map_iff {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) {x : β} {I : Interval α} : x ∈ I.map f ↔ (∀ (a : α), I.lb = ↑a → f a ≤ x) ∧ ∀ (a : α), I.ub = ↑a → x ≤ f a

def Inclusion.Interval.univ (α : Type u_3) : Interval α

The interval unbounded on both sides.

Equations

• Inclusion.Interval.univ α = { lb := ⊥, ub := ⊤ }

@[instance_reducible]

instance Inclusion.instUnivInterval {α : Type u_1} [Preorder α] : Univ (Interval α) α

Equations

• Inclusion.instUnivInterval = { univ := Inclusion.Interval.univ α, mem_univ := ⋯ }

theorem Inclusion.Interval.mem_map_univ {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) (x : β) : x ∈ (univ α).map f

def Inclusion.Interval.singleton {α : Type u_1} (a : α) : Interval α

The interval whose two endpoints are a.

Equations

• Inclusion.Interval.singleton a = { lb := ↑a, ub := ↑a }

theorem Inclusion.Interval.mem_map_singleton {α : Type u_1} {β : Type u_2} [Preorder β] (a : α) (f : α → β) : f a ∈ (singleton a).map f

def Inclusion.Interval.Icc {α : Type u_1} (lb : WithBot α) (ub : WithTop α) : Interval α

The interval with lower endpoint lb and upper endpoint ub.

Equations

• Inclusion.Interval.Icc lb ub = { lb := lb, ub := ub }

theorem Inclusion.Interval.mem_map_Icc {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) {lb ub : α} {x : β} (hl : f lb ≤ x) (hu : x ≤ f ub) : x ∈ (Icc ↑lb ↑ub).map f

theorem Inclusion.Interval.map_lb_le {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) {lb : α} {ub : WithTop α} {x : β} (hx : x ∈ (Icc (↑lb) ub).map f) : f lb ≤ x

theorem Inclusion.Interval.le_map_ub {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) {lb : WithBot α} {ub : α} {x : β} (hx : x ∈ (Icc lb ↑ub).map f) : x ≤ f ub

def Inclusion.Interval.Iic {α : Type u_1} (ub : WithTop α) : Interval α

The interval unbounded below with upper endpoint ub.

Equations

• Inclusion.Interval.Iic ub = { lb := ⊥, ub := ub }

def Inclusion.Interval.Ici {α : Type u_1} (lb : WithBot α) : Interval α

The interval unbounded above with lower endpoint lb.

Equations

• Inclusion.Interval.Ici lb = { lb := lb, ub := ⊤ }

theorem Inclusion.Interval.mem_Iic_of_le {α : Type u_1} [Preorder α] {x y : α} {I : Interval α} (hxy : x ≤ y) (hy : y ∈ I) : x ∈ Iic I.ub

theorem Inclusion.Interval.mem_Ici_of_le {α : Type u_1} [Preorder α] {x y : α} {I : Interval α} (hxy : x ≤ y) (hx : x ∈ I) : y ∈ Ici I.lb

theorem Inclusion.Interval.mem_Icc_of_le {α : Type u_1} [Preorder α] {a b x : α} {I J : Interval α} (ha : a ∈ I) (hax : a ≤ x) (hxb : x ≤ b) (hb : b ∈ J) : x ∈ Icc I.lb J.ub

theorem Inclusion.Interval.mem_Iic_of_lt {α : Type u_1} [Preorder α] {x y : α} {I : Interval α} (hxy : x < y) (hy : y ∈ I) : x ∈ Iic I.ub

theorem Inclusion.Interval.mem_Ici_of_lt {α : Type u_1} [Preorder α] {x y : α} {I : Interval α} (hxy : x < y) (hx : x ∈ I) : y ∈ Ici I.lb

theorem Inclusion.Interval.mem_Ici_of_mem_Ici {α : Type u_1} [Preorder α] {a x : α} {I : Interval α} (hx : x ∈ Set.Ici a) (ha : a ∈ I) : x ∈ Ici I.lb

theorem Inclusion.Interval.mem_Ici_of_mem_Ioi {α : Type u_1} [Preorder α] {a x : α} {I : Interval α} (hx : x ∈ Set.Ioi a) (ha : a ∈ I) : x ∈ Ici I.lb

theorem Inclusion.Interval.mem_Iic_of_mem_Iic {α : Type u_1} [Preorder α] {b x : α} {I : Interval α} (hx : x ∈ Set.Iic b) (hb : b ∈ I) : x ∈ Iic I.ub

theorem Inclusion.Interval.mem_Iic_of_mem_Iio {α : Type u_1} [Preorder α] {b x : α} {I : Interval α} (hx : x ∈ Set.Iio b) (hb : b ∈ I) : x ∈ Iic I.ub

theorem Inclusion.Interval.mem_Icc_of_mem_Ico {α : Type u_1} [Preorder α] {a b x : α} {I J : Interval α} (hx : x ∈ Set.Ico a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Icc I.lb J.ub

theorem Inclusion.Interval.mem_Icc_of_mem_Ioc {α : Type u_1} [Preorder α] {a b x : α} {I J : Interval α} (hx : x ∈ Set.Ioc a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Icc I.lb J.ub

theorem Inclusion.Interval.mem_Icc_of_mem_Icc {α : Type u_1} [Preorder α] {a b x : α} {I J : Interval α} (hx : x ∈ Set.Icc a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Icc I.lb J.ub

theorem Inclusion.Interval.mem_Icc_of_mem_Ioo {α : Type u_1} [Preorder α] {a b x : α} {I J : Interval α} (hx : x ∈ Set.Ioo a b) (ha : a ∈ I) (hb : b ∈ J) : x ∈ Icc I.lb J.ub

def Inclusion.Interval.inter {α : Type u_1} [LinearOrder α] (I J : Interval α) : Interval α

The intersection of two intervals.

Equations

• I.inter J = { lb := max I.lb J.lb, ub := min I.ub J.ub }

@[instance_reducible]

instance Inclusion.instRefineInterval {α : Type u_1} [LinearOrder α] : Refine (Interval α) α

Equations

• Inclusion.instRefineInterval = { refine := Inclusion.Interval.inter, mem_refine := ⋯ }

@[simp]

theorem Inclusion.Interval.map_inter {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ↪o β) (I J : Interval α) : (I.inter J).map ⇑f = (I.map ⇑f).inter (J.map ⇑f)

theorem Inclusion.Interval.inter_mem {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ↪o β) {x : β} {I J : Interval α} (hxI : x ∈ I.map ⇑f) (hxJ : x ∈ J.map ⇑f) : x ∈ (I.inter J).map ⇑f

def Inclusion.Interval.hull {α : Type u_1} [LinearOrder α] (I J : Interval α) : Interval α

The convex hull of two intervals.

Equations

• I.hull J = { lb := min I.lb J.lb, ub := max I.ub J.ub }

theorem Inclusion.Interval.mem_hull_left {α : Type u_1} [LinearOrder α] {x : α} {I J : Interval α} (hx : x ∈ I) : x ∈ I.hull J

theorem Inclusion.Interval.mem_hull_right {α : Type u_1} [LinearOrder α] {x : α} {I J : Interval α} (hx : x ∈ J) : x ∈ I.hull J

@[instance_reducible]

instance Inclusion.instCoarsenInterval {α : Type u_1} [LinearOrder α] : Coarsen (Interval α) α

Equations

• Inclusion.instCoarsenInterval = { coarsen := Inclusion.Interval.hull, mem_coarsen_left := ⋯, mem_coarsen_right := ⋯ }

@[simp]

theorem Inclusion.Interval.map_hull {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ↪o β) (I J : Interval α) : (I.hull J).map ⇑f = (I.map ⇑f).hull (J.map ⇑f)

theorem Inclusion.Interval.hull_mem_left {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ↪o β) {x : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) : x ∈ (I.hull J).map ⇑f

theorem Inclusion.Interval.hull_mem_right {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ↪o β) {x : β} {I J : Interval α} (hx : x ∈ J.map ⇑f) : x ∈ (I.hull J).map ⇑f

def Inclusion.Interval.add {α : Type u_1} [Add α] (I J : Interval α) : Interval α

Add two intervals.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Inclusion.Interval.add_lb {α : Type u_1} [AddZero α] (I J : Interval α) : (I.add J).lb = I.lb + J.lb

@[simp]

theorem Inclusion.Interval.add_ub {α : Type u_1} [AddZero α] (I J : Interval α) : (I.add J).ub = I.ub + J.ub

theorem Inclusion.Interval.add_mem {α : Type u_1} {β : Type u_2} [AddZero α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α →+ β) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : x + y ∈ (I.add J).map ⇑f

def Inclusion.Interval.neg {α : Type u_1} [Neg α] (I : Interval α) : Interval α

Negate an interval.

Equations

• I.neg = { lb := match I.ub with | some a => some (-a) | none => ⊥, ub := match I.lb with | some a => some (-a) | none => ⊤ }

theorem Inclusion.Interval.neg_mem {α : Type u_1} {β : Type u_2} [AddGroup α] [AddCommGroup β] [Preorder β] [IsOrderedAddMonoid β] (f : α →+ β) {x : β} {I : Interval α} (hx : x ∈ I.map ⇑f) : -x ∈ I.neg.map ⇑f

def Inclusion.Interval.sub {α : Type u_1} [Sub α] (I J : Interval α) : Interval α

Subtract one interval from another.

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.Interval.sub_eq_add_neg {α : Type u_1} [AddGroup α] (I J : Interval α) : I.sub J = I.add J.neg

theorem Inclusion.Interval.sub_mem {α : Type u_1} {β : Type u_2} [AddGroup α] [AddCommGroup β] [Preorder β] [IsOrderedAddMonoid β] (f : α →+ β) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : x - y ∈ (I.sub J).map ⇑f

def Inclusion.Interval.mulBound {α : Type u_1} [Mul α] [Zero α] [DecidableEq α] : Option α → Option α → Option α

Multiply two finite or infinite interval bounds.

Equations

• Inclusion.Interval.mulBound (some a) (some b) = some (a * b)
• Inclusion.Interval.mulBound (some a) none = if a = 0 then some 0 else none
• Inclusion.Interval.mulBound none (some b) = if b = 0 then some 0 else none
• Inclusion.Interval.mulBound none none = none

theorem Inclusion.Interval.map_mulBound_le {α : Type u_1} {β : Type u_2} [Mul α] [Zero α] [DecidableEq α] [LE β] (f : α → β) (a b : Option α) {z : β} (hmul : ∀ (x y : α), a = some x → b = some y → f (x * y) ≤ z) (hzero : a = none ∧ b = some 0 ∨ a = some 0 ∧ b = none → f 0 ≤ z) : WithBot.map f (mulBound a b) ≤ ↑z

theorem Inclusion.Interval.le_map_mulBound {α : Type u_1} {β : Type u_2} [Mul α] [Zero α] [DecidableEq α] [LE β] (f : α → β) (a b : Option α) {z : β} (hmul : ∀ (x y : α), a = some x → b = some y → z ≤ f (x * y)) (hzero : a = none ∧ b = some 0 ∨ a = some 0 ∧ b = none → z ≤ f 0) : ↑z ≤ WithTop.map f (mulBound a b)

def Inclusion.Interval.mul {α : Type u_1} [Mul α] [Zero α] [LinearOrder α] (I J : Interval α) : Interval α

Multiply two intervals.

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.Interval.mul_mem {α : Type u_1} {β : Type u_2} [Mul α] [Zero α] [LinearOrder α] [Ring β] [LinearOrder β] [IsStrictOrderedRing β] (f : α ↪o β) (map_zero : f 0 = 0) (map_mul : ∀ (a b : α), f (a * b) = f a * f b) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : x * y ∈ (I.mul J).map ⇑f

def Inclusion.Interval.orderRelFalse {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (I J : Interval α) : IntervalBool

Check if r x y is false is implied by x ∈ I and y ∈ J

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.Interval.orderRelFalse_mem {α : Type u_1} {β : Type u_2} [Preorder β] {r : α → α → Prop} {s : β → β → Prop} [DecidableRel r] [Trans (fun (x1 x2 : β) => x1 ≤ x2) s s] [Trans s (fun (x1 x2 : β) => x1 ≤ x2) s] (f : r ↪r s) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : s x y ∈ orderRelFalse r I J

def Inclusion.Interval.orderRel {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (I J : Interval α) : IntervalBool

Check if r x y is implied (true or false) by x ∈ I and y ∈ J.

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.Interval.orderRel_mem {α : Type u_1} {β : Type u_2} [Preorder β] {r : α → α → Prop} {s : β → β → Prop} [DecidableRel r] [Trans (fun (x1 x2 : β) => x1 ≤ x2) s s] [Trans s (fun (x1 x2 : β) => x1 ≤ x2) s] (f : r ↪r s) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : s x y ∈ orderRel r I J

def Inclusion.Interval.le {α : Type u_1} [LE α] [DecidableLE α] (I J : Interval α) : IntervalBool

Check if x ≤ y is implied (true or false) by x ∈ I and y ∈ J

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.Interval.le_mem {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLE α] (f : α ↪o β) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : x ≤ y ∈ I.le J

def Inclusion.Interval.lt {α : Type u_1} [LT α] [DecidableLT α] (I J : Interval α) : IntervalBool

Check if x < y is implied (true or false) by x ∈ I and y ∈ J.

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.Interval.lt_mem {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLT α] (f : α ↪o β) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : x < y ∈ I.lt J

def Inclusion.Interval.eq {α : Type u_1} [LE α] [DecidableLE α] (I J : Interval α) : IntervalBool

Check if x = y is implied (true or false) by x ∈ I and y ∈ J.

Equations

• I.eq J = (I.le J).and (J.le I)

theorem Inclusion.Interval.eq_mem {α : Type u_1} {β : Type u_2} [Preorder α] [PartialOrder β] [DecidableLE α] (f : α ↪o β) {x y : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hy : y ∈ J.map ⇑f) : x = y ∈ I.eq J

theorem Inclusion.Interval.mem_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLE α] (f : α ↪o β) {a x : β} {I J : Interval α} (ha : a ∈ I.map ⇑f) (hx : x ∈ J.map ⇑f) : (x ∈ Set.Ici a) ∈ I.le J

theorem Inclusion.Interval.mem_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLT α] (f : α ↪o β) {a x : β} {I J : Interval α} (ha : a ∈ I.map ⇑f) (hx : x ∈ J.map ⇑f) : (x ∈ Set.Ioi a) ∈ I.lt J

theorem Inclusion.Interval.mem_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLE α] (f : α ↪o β) {b x : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hb : b ∈ J.map ⇑f) : (x ∈ Set.Iic b) ∈ I.le J

theorem Inclusion.Interval.mem_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLT α] (f : α ↪o β) {b x : β} {I J : Interval α} (hx : x ∈ I.map ⇑f) (hb : b ∈ J.map ⇑f) : (x ∈ Set.Iio b) ∈ I.lt J

theorem Inclusion.Interval.mem_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLE α] (f : α ↪o β) {a b x : β} {I J K : Interval α} (ha : a ∈ I.map ⇑f) (hx : x ∈ J.map ⇑f) (hb : b ∈ K.map ⇑f) : (x ∈ Set.Icc a b) ∈ (I.le J).and (J.le K)

theorem Inclusion.Interval.mem_Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLE α] [DecidableLT α] (f : α ↪o β) {a b x : β} {I J K : Interval α} (ha : a ∈ I.map ⇑f) (hx : x ∈ J.map ⇑f) (hb : b ∈ K.map ⇑f) : (x ∈ Set.Ico a b) ∈ (I.le J).and (J.lt K)

theorem Inclusion.Interval.mem_Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLE α] [DecidableLT α] (f : α ↪o β) {a b x : β} {I J K : Interval α} (ha : a ∈ I.map ⇑f) (hx : x ∈ J.map ⇑f) (hb : b ∈ K.map ⇑f) : (x ∈ Set.Ioc a b) ∈ (I.lt J).and (J.le K)

theorem Inclusion.Interval.mem_Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DecidableLT α] (f : α ↪o β) {a b x : β} {I J K : Interval α} (ha : a ∈ I.map ⇑f) (hx : x ∈ J.map ⇑f) (hb : b ∈ K.map ⇑f) : (x ∈ Set.Ioo a b) ∈ (I.lt J).and (J.lt K)