# Documentation

Mathlib.Order.Interval

# Order intervals #

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

## Main declarations #

• NonemptyInterval: Nonempty intervals. Pairs where the second element is greater than the first.
• Interval: Intervals. Either ∅ or a nonempty interval.
structure NonemptyInterval (α : Type u_7) [LE α] extends :
Type u_7
• fst : α
• snd : α
• fst_le_snd : s.fst s.snd

The starting point of an interval is smaller than the endpoint.

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 NonemptyInterval α → Set α.

Instances For
theorem NonemptyInterval.toProd_injective {α : Type u_1} [LE α] :
Function.Injective NonemptyInterval.toProd
theorem NonemptyInterval.ext {α : Type u_1} [LE α] (s : ) (t : ) (h : s.toProd = t.toProd) :
s = t
theorem NonemptyInterval.ext_iff {α : Type u_1} [LE α] (s : ) (t : ) :
s = t s.toProd = t.toProd
def NonemptyInterval.toDualProd {α : Type u_1} [LE α] :
αᵒᵈ × α

The injection that induces the order on intervals.

Instances For
@[simp]
theorem NonemptyInterval.toDualProd_apply {α : Type u_1} [LE α] (s : ) :
= (OrderDual.toDual s.fst, s.snd)
theorem NonemptyInterval.toDualProd_injective {α : Type u_1} [LE α] :
Function.Injective NonemptyInterval.toDualProd
instance NonemptyInterval.le {α : Type u_1} [LE α] :
theorem NonemptyInterval.le_def {α : Type u_1} [LE α] {s : } {t : } :
s t t.fst s.fst s.snd t.snd
@[simp]
theorem NonemptyInterval.toDualProdHom_apply {α : Type u_1} [LE α] :
∀ (a : ), NonemptyInterval.toDualProdHom a =
def NonemptyInterval.toDualProdHom {α : Type u_1} [LE α] :
↪o αᵒᵈ × α

toDualProd as an order embedding.

Instances For
def NonemptyInterval.dual {α : Type u_1} [LE α] :

Turn an interval into an interval in the dual order.

Instances For
@[simp]
theorem NonemptyInterval.fst_dual {α : Type u_1} [LE α] (s : ) :
(NonemptyInterval.dual s).fst = OrderDual.toDual s.snd
@[simp]
theorem NonemptyInterval.snd_dual {α : Type u_1} [LE α] (s : ) :
(NonemptyInterval.dual s).snd = OrderDual.toDual s.fst
@[simp]
theorem NonemptyInterval.mem_mk {α : Type u_1} [] {x : α × α} {a : α} {hx : x.fst x.snd} :
a { toProd := x, fst_le_snd := hx } x.fst a a x.snd
theorem NonemptyInterval.mem_def {α : Type u_1} [] {s : } {a : α} :
a s s.fst a a s.snd
theorem NonemptyInterval.coe_nonempty {α : Type u_1} [] (s : ) :
Set.Nonempty (Set.Icc s.fst s.snd)
@[simp]
theorem NonemptyInterval.pure_fst {α : Type u_1} [] (a : α) :
().toProd.fst = a
@[simp]
theorem NonemptyInterval.pure_snd {α : Type u_1} [] (a : α) :
().toProd.snd = a
def NonemptyInterval.pure {α : Type u_1} [] (a : α) :

{a} as an interval.

Instances For
theorem NonemptyInterval.mem_pure_self {α : Type u_1} [] (a : α) :
theorem NonemptyInterval.pure_injective {α : Type u_1} [] :
Function.Injective NonemptyInterval.pure
@[simp]
theorem NonemptyInterval.dual_pure {α : Type u_1} [] (a : α) :
NonemptyInterval.dual () = NonemptyInterval.pure (OrderDual.toDual a)
@[simp]
theorem NonemptyInterval.map_snd {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (a : ) :
().toProd.snd = f a.1.snd
@[simp]
theorem NonemptyInterval.map_fst {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (a : ) :
().toProd.fst = f a.1.fst
def NonemptyInterval.map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (a : ) :

Pushforward of nonempty intervals.

Instances For
@[simp]
theorem NonemptyInterval.map_pure {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (a : α) :
@[simp]
theorem NonemptyInterval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : β →o γ) (f : α →o β) (a : ) :
@[simp]
theorem NonemptyInterval.dual_map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (a : ) :
NonemptyInterval.dual () = NonemptyInterval.map (OrderHom.dual f) (NonemptyInterval.dual a)
@[simp]
theorem NonemptyInterval.map₂_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :
∀ (a : ) (a_1 : ), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.snd = f a.snd a_1.snd
@[simp]
theorem NonemptyInterval.map₂_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :
∀ (a : ) (a_1 : ), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.fst = f a.fst a_1.fst
def NonemptyInterval.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :

Binary pushforward of nonempty intervals.

Instances For
@[simp]
theorem NonemptyInterval.map₂_pure {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (a : α) (b : β) :
@[simp]
theorem NonemptyInterval.dual_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (s : ) (t : ) :
NonemptyInterval.dual (NonemptyInterval.map₂ f h₀ h₁ s t) = NonemptyInterval.map₂ (fun a b => OrderDual.toDual (f (OrderDual.ofDual a) (OrderDual.ofDual b))) (_ : ∀ (x : βᵒᵈ), Monotone (OrderDual.toDual (fun a => f a (OrderDual.ofDual x)) OrderDual.ofDual)) (_ : ∀ (x : αᵒᵈ), Monotone (OrderDual.toDual f (OrderDual.ofDual x) OrderDual.ofDual)) (NonemptyInterval.dual s) (NonemptyInterval.dual t)
@[simp]
theorem NonemptyInterval.dual_top {α : Type u_1} [] [] :
NonemptyInterval.dual =
def NonemptyInterval.coeHom {α : Type u_1} [] :

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

Instances For
instance NonemptyInterval.setLike {α : Type u_1} [] :
theorem NonemptyInterval.coe_subset_coe {α : Type u_1} [] {s : } {t : } :
s t s t
theorem NonemptyInterval.coe_ssubset_coe {α : Type u_1} [] {s : } {t : } :
s t s < t
@[simp]
theorem NonemptyInterval.coe_coeHom {α : Type u_1} [] :
NonemptyInterval.coeHom = SetLike.coe
@[simp]
theorem NonemptyInterval.coe_pure {α : Type u_1} [] (a : α) :
= {a}
@[simp]
theorem NonemptyInterval.mem_pure {α : Type u_1} [] {a : α} {b : α} :
b = a
@[simp]
theorem NonemptyInterval.coe_top {α : Type u_1} [] [] :
= Set.univ
@[simp]
theorem NonemptyInterval.coe_dual {α : Type u_1} [] (s : ) :
↑(NonemptyInterval.dual s) = OrderDual.ofDual ⁻¹' s
theorem NonemptyInterval.subset_coe_map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (s : ) :
f '' s ↑()
@[simp]
theorem NonemptyInterval.fst_sup {α : Type u_1} [] (s : ) (t : ) :
(s t).fst = s.fst t.fst
@[simp]
theorem NonemptyInterval.snd_sup {α : Type u_1} [] (s : ) (t : ) :
(s t).snd = s.snd t.snd
@[reducible]
def Interval (α : Type u_7) [LE α] :
Type u_7

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 α.

Instances For
instance Interval.instInhabitedInterval {α : Type u_1} [LE α] :
instance Interval.instLEInterval {α : Type u_1} [LE α] :
LE ()
instance Interval.canLift {α : Type u_1} [LE α] :
CanLift () () WithBot.some fun r => r
theorem Interval.coe_injective {α : Type u_1} [LE α] :
Function.Injective WithBot.some
theorem Interval.coe_inj {α : Type u_1} [LE α] {s : } {t : } :
s = t s = t
theorem Interval.forall {α : Type u_1} [LE α] {p : Prop} :
((s : ) → p s) p ((s : ) → p s)
theorem Interval.exists {α : Type u_1} [LE α] {p : Prop} :
(s, p s) p s, p s
instance Interval.instUniqueInterval {α : Type u_1} [LE α] [] :
def Interval.dual {α : Type u_1} [LE α] :

Turn an interval into an interval in the dual order.

Instances For
def Interval.pure {α : Type u_1} [] (a : α) :

{a} as an interval.

Instances For
theorem Interval.pure_injective {α : Type u_1} [] :
Function.Injective Interval.pure
@[simp]
theorem Interval.dual_pure {α : Type u_1} [] (a : α) :
Interval.dual () = Interval.pure (OrderDual.toDual a)
@[simp]
theorem Interval.dual_bot {α : Type u_1} [] :
Interval.dual =
@[simp]
theorem Interval.pure_ne_bot {α : Type u_1} [] {a : α} :
@[simp]
theorem Interval.bot_ne_pure {α : Type u_1} [] {a : α} :
def Interval.map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) :

Pushforward of intervals.

Instances For
@[simp]
theorem Interval.map_pure {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (a : α) :
= Interval.pure (f a)
@[simp]
theorem Interval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : β →o γ) (f : α →o β) (s : ) :
@[simp]
theorem Interval.dual_map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (s : ) :
Interval.dual () = Interval.map (OrderHom.dual f) (Interval.dual s)
instance Interval.boundedOrder {α : Type u_1} [] [] :
@[simp]
theorem Interval.dual_top {α : Type u_1} [] [] :
Interval.dual =
instance Interval.partialOrder {α : Type u_1} [] :
def Interval.coeHom {α : Type u_1} [] :
↪o Set α

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

Instances For
instance Interval.setLike {α : Type u_1} [] :
SetLike () α
theorem Interval.coe_subset_coe {α : Type u_1} [] {s : } {t : } :
s t s t
theorem Interval.coe_sSubset_coe {α : Type u_1} [] {s : } {t : } :
s t s < t
@[simp]
theorem Interval.coe_pure {α : Type u_1} [] (a : α) :
↑() = {a}
@[simp]
theorem Interval.coe_coe {α : Type u_1} [] (s : ) :
s = s
@[simp]
theorem Interval.coe_bot {α : Type u_1} [] :
=
@[simp]
theorem Interval.coe_top {α : Type u_1} [] [] :
= Set.univ
@[simp]
theorem Interval.coe_dual {α : Type u_1} [] (s : ) :
↑(Interval.dual s) = OrderDual.ofDual ⁻¹' s
theorem Interval.subset_coe_map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) (s : ) :
f '' s ↑()
@[simp]
theorem Interval.mem_pure {α : Type u_1} [] {a : α} {b : α} :
b = a
theorem Interval.mem_pure_self {α : Type u_1} [] (a : α) :
instance Interval.semilatticeSup {α : Type u_1} [] :
instance Interval.lattice {α : Type u_1} [] [DecidableRel fun x x_1 => x x_1] :
@[simp]
theorem Interval.coe_inf {α : Type u_1} [] [DecidableRel fun x x_1 => x x_1] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem Interval.disjoint_coe {α : Type u_1} [] (s : ) (t : ) :
Disjoint s t Disjoint s t
@[simp]
theorem NonemptyInterval.coe_pure_interval {α : Type u_1} [] (a : α) :
@[simp]
theorem NonemptyInterval.coe_eq_pure {α : Type u_1} [] {s : } {a : α} :
s =
@[simp]
theorem NonemptyInterval.coe_top_interval {α : Type u_1} [] [] :
=
@[simp]
theorem NonemptyInterval.mem_coe_interval {α : Type u_1} [] {s : } {x : α} :
x s x s
@[simp]
theorem NonemptyInterval.coe_sup_interval {α : Type u_1} [] (s : ) (t : ) :
↑(s t) = s t
noncomputable instance Interval.completeLattice {α : Type u_1} [] [DecidableRel fun x x_1 => x x_1] :
@[simp]
theorem Interval.coe_sInf {α : Type u_1} [] [DecidableRel fun x x_1 => x x_1] (S : Set ()) :
↑(sInf S) = ⋂ (s : ) (_ : s S), s
@[simp]
theorem Interval.coe_iInf {α : Type u_1} {ι : Sort u_5} [] [DecidableRel fun x x_1 => x x_1] (f : ι) :
↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)
theorem Interval.coe_iInf₂ {α : Type u_1} {ι : Sort u_5} {κ : ιSort u_6} [] [DecidableRel fun x x_1 => x x_1] (f : (i : ι) → κ i) :
↑(⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)