order.interval

# Order intervals #

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

This file defines (nonempty) closed intervals in an order (see set.Icc). This is a prototype for interval arithmetic.

## Main declarations #

• nonempty_interval: Nonempty intervals. Pairs where the second element is greater than the first.
• interval: Intervals. Either ∅ or a nonempty interval.
theorem nonempty_interval.ext {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) (h : x.to_prod = y.to_prod) :
x = y
@[ext]
structure nonempty_interval (α : Type u_7) [has_le α] :
Type u_7

The nonempty closed intervals in an order.

We define intervals by the pair of endpoints fst, snd. To convert intervals to the set of elements between these endpoints, use the coercion nonempty_interval α → set α.

Instances for nonempty_interval
theorem nonempty_interval.ext_iff {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) :
def nonempty_interval.to_dual_prod {α : Type u_1} [has_le α] :
αᵒᵈ × α

The injection that induces the order on intervals.

Equations
@[protected, instance]
def nonempty_interval.is_empty {α : Type u_1} [has_le α] [is_empty α] :
@[protected, instance]
@[protected, instance]
def nonempty_interval.has_le {α : Type u_1} [has_le α] :
Equations

to_dual_prod as an order embedding.

Equations
@[simp]
def nonempty_interval.dual {α : Type u_1} [has_le α] :

Turn an interval into an interval in the dual order.

Equations
@[simp]
theorem nonempty_interval.fst_dual {α : Type u_1} [has_le α] (s : nonempty_interval α) :
@[simp]
theorem nonempty_interval.snd_dual {α : Type u_1} [has_le α] (s : nonempty_interval α) :
@[protected, instance]
def nonempty_interval.preorder {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def nonempty_interval.set.has_coe_t {α : Type u_1} [preorder α] :
(set α)
Equations
@[protected, instance]
def nonempty_interval.has_mem {α : Type u_1} [preorder α] :
Equations
@[simp]
theorem nonempty_interval.mem_mk {α : Type u_1} [preorder α] {x : α × α} {a : α} {hx : x.fst x.snd} :
a {to_prod := x, fst_le_snd := hx} x.fst a a x.snd
theorem nonempty_interval.mem_def {α : Type u_1} [preorder α] {s : nonempty_interval α} {a : α} :
@[simp]
theorem nonempty_interval.coe_nonempty {α : Type u_1} [preorder α] (s : nonempty_interval α) :
@[simp]
theorem nonempty_interval.pure_to_prod {α : Type u_1} [preorder α] (a : α) :
= (a, a)
def nonempty_interval.pure {α : Type u_1} [preorder α] (a : α) :

{a} as an interval.

Equations
theorem nonempty_interval.mem_pure_self {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem nonempty_interval.dual_pure {α : Type u_1} [preorder α] (a : α) :
@[protected, instance]
def nonempty_interval.inhabited {α : Type u_1} [preorder α] [inhabited α] :
Equations
@[protected, instance]
def nonempty_interval.nonempty {α : Type u_1} [preorder α] [nonempty α] :
@[protected, instance]
@[simp]
theorem nonempty_interval.map_to_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :
def nonempty_interval.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :

Pushforward of nonempty intervals.

Equations
@[simp]
theorem nonempty_interval.map_pure {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : α) :
@[simp]
theorem nonempty_interval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) (a : nonempty_interval α) :
= a
@[simp]
theorem nonempty_interval.dual_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :
@[simp]
theorem nonempty_interval.map₂_to_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α β γ) (h₀ : (b : β), monotone (λ (a : α), f a b)) (h₁ : (a : α), monotone (f a)) (ᾰ : nonempty_interval α) (ᾰ_1 : nonempty_interval β) :
h₁ ᾰ_1).to_prod = (f ᾰ.to_prod.fst ᾰ_1.to_prod.fst, f ᾰ.to_prod.snd ᾰ_1.to_prod.snd)
def nonempty_interval.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α β γ) (h₀ : (b : β), monotone (λ (a : α), f a b)) (h₁ : (a : α), monotone (f a)) :

Binary pushforward of nonempty intervals.

Equations
@[simp]
theorem nonempty_interval.map₂_pure {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α β γ) (h₀ : (b : β), monotone (λ (a : α), f a b)) (h₁ : (a : α), monotone (f a)) (a : α) (b : β) :
@[simp]
theorem nonempty_interval.dual_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α β γ) (h₀ : (b : β), monotone (λ (a : α), f a b)) (h₁ : (a : α), monotone (f a)) (s : nonempty_interval α) (t : nonempty_interval β) :
@[protected, instance]
def nonempty_interval.order_top {α : Type u_1} [preorder α]  :
Equations
@[simp]
theorem nonempty_interval.dual_top {α : Type u_1} [preorder α]  :
@[protected, instance]
Equations
def nonempty_interval.coe_hom {α : Type u_1}  :

Consider a nonempty interval [a, b] as the set [a, b].

Equations
@[protected, instance]
def nonempty_interval.set_like {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem nonempty_interval.coe_subset_coe {α : Type u_1} {s t : nonempty_interval α} :
s t s t
@[simp, norm_cast]
theorem nonempty_interval.coe_ssubset_coe {α : Type u_1} {s t : nonempty_interval α} :
s t s < t
@[simp]
theorem nonempty_interval.coe_coe_hom {α : Type u_1}  :
@[simp, norm_cast]
theorem nonempty_interval.coe_pure {α : Type u_1} (a : α) :
= {a}
@[simp]
theorem nonempty_interval.mem_pure {α : Type u_1} {a b : α} :
b = a
@[simp, norm_cast]
theorem nonempty_interval.coe_top {α : Type u_1}  :
@[simp, norm_cast]
theorem nonempty_interval.coe_dual {α : Type u_1} (s : nonempty_interval α) :
theorem nonempty_interval.subset_coe_map {α : Type u_1} {β : Type u_2} (f : α →o β) (s : nonempty_interval α) :
@[protected, instance]
def nonempty_interval.has_sup {α : Type u_1} [lattice α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem nonempty_interval.fst_sup {α : Type u_1} [lattice α] (s t : nonempty_interval α) :
@[simp]
theorem nonempty_interval.snd_sup {α : Type u_1} [lattice α] (s t : nonempty_interval α) :
@[protected, instance]
def interval.has_le (α : Type u_1) [has_le α] :
def interval (α : Type u_1) [has_le α] :
Type u_1

The closed intervals in an order.

We represent intervals either as ⊥ or a nonempty interval given by its endpoints fst, snd. To convert intervals to the set of elements between these endpoints, use the coercion interval α → set α.

Equations
Instances for interval
@[protected, instance]
def interval.inhabited (α : Type u_1) [has_le α] :
@[protected, instance]
def interval.order_bot (α : Type u_1) [has_le α] :
@[protected, instance]
def interval.has_coe_t {α : Type u_1} [has_le α] :
(interval α)
Equations
@[protected, instance]
def interval.can_lift {α : Type u_1} [has_le α] :
can_lift (interval α) coe (λ (r : interval α), r )
Equations
theorem interval.coe_injective {α : Type u_1} [has_le α] :
@[simp, norm_cast]
theorem interval.coe_inj {α : Type u_1} [has_le α] {s t : nonempty_interval α} :
s = t s = t
@[protected]
theorem interval.forall {α : Type u_1} [has_le α] {p : Prop} :
( (s : interval α), p s) p (s : , p s
@[protected]
theorem interval.exists {α : Type u_1} [has_le α] {p : Prop} :
( (s : interval α), p s) p (s : , p s
@[protected, instance]
def interval.unique {α : Type u_1} [has_le α] [is_empty α] :
Equations
def interval.dual {α : Type u_1} [has_le α] :

Turn an interval into an interval in the dual order.

Equations
@[protected, instance]
def interval.preorder {α : Type u_1} [preorder α] :
Equations
def interval.pure {α : Type u_1} [preorder α] (a : α) :

{a} as an interval.

Equations
theorem interval.pure_injective {α : Type u_1} [preorder α] :
@[simp]
theorem interval.dual_pure {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem interval.dual_bot {α : Type u_1} [preorder α] :
@[simp]
theorem interval.pure_ne_bot {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem interval.bot_ne_pure {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def interval.nontrivial {α : Type u_1} [preorder α] [nonempty α] :
def interval.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) :

Pushforward of intervals.

Equations
@[simp]
theorem interval.map_pure {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : α) :
@[simp]
theorem interval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (g : β →o γ) (f : α →o β) (s : interval α) :
s) = interval.map (g.comp f) s
@[simp]
theorem interval.dual_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (s : interval α) :
=
@[protected, instance]
def interval.bounded_order {α : Type u_1} [preorder α]  :
Equations
@[simp]
theorem interval.dual_top {α : Type u_1} [preorder α]  :
@[protected, instance]
def interval.partial_order {α : Type u_1}  :
Equations
def interval.coe_hom {α : Type u_1}  :
↪o set α

Consider a interval [a, b] as the set [a, b].

Equations
@[protected, instance]
def interval.set_like {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem interval.coe_subset_coe {α : Type u_1} {s t : interval α} :
s t s t
@[simp, norm_cast]
theorem interval.coe_ssubset_coe {α : Type u_1} {s t : interval α} :
s t s < t
@[simp, norm_cast]
theorem interval.coe_pure {α : Type u_1} (a : α) :
= {a}
@[simp, norm_cast]
theorem interval.coe_coe {α : Type u_1} (s : nonempty_interval α) :
@[simp, norm_cast]
theorem interval.coe_bot {α : Type u_1}  :
@[simp, norm_cast]
theorem interval.coe_top {α : Type u_1}  :
@[simp, norm_cast]
theorem interval.coe_dual {α : Type u_1} (s : interval α) :
theorem interval.subset_coe_map {α : Type u_1} {β : Type u_2} (f : α →o β) (s : interval α) :
@[simp]
theorem interval.mem_pure {α : Type u_1} {a b : α} :
b = a
theorem interval.mem_pure_self {α : Type u_1} (a : α) :
@[protected, instance]
def interval.semilattice_sup {α : Type u_1} [lattice α] :
Equations
@[protected, instance]
def interval.lattice {α : Type u_1} [lattice α]  :
Equations
@[simp, norm_cast]
theorem interval.coe_inf {α : Type u_1} [lattice α] (s t : interval α) :
(s t) = s t
@[simp, norm_cast]
theorem interval.disjoint_coe {α : Type u_1} [lattice α] (s t : interval α) :
t t
@[simp, norm_cast]
theorem nonempty_interval.coe_pure_interval {α : Type u_1} [preorder α] (a : α) :
@[simp, norm_cast]
theorem nonempty_interval.coe_eq_pure {α : Type u_1} [preorder α] {s : nonempty_interval α} {a : α} :
@[simp, norm_cast]
theorem nonempty_interval.coe_top_interval {α : Type u_1} [preorder α]  :
@[simp, norm_cast]
theorem nonempty_interval.mem_coe_interval {α : Type u_1} {s : nonempty_interval α} {x : α} :
x s x s
@[simp, norm_cast]
theorem nonempty_interval.coe_sup_interval {α : Type u_1} [lattice α] (s t : nonempty_interval α) :
(s t) = s t
@[protected, instance]
noncomputable def interval.complete_lattice {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem interval.coe_Inf {α : Type u_1} (S : set (interval α)) :
(has_Inf.Inf S) = (s : interval α) (H : s S), s
@[simp, norm_cast]
theorem interval.coe_infi {α : Type u_1} {ι : Sort u_5} (f : ι ) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem interval.coe_infi₂ {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_6} (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)