mathlib documentation

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 #

theorem nonempty_interval.ext {α : Type u_6} {_inst_1 : has_le α} (x y : nonempty_interval α) (h : x.to_prod = y.to_prod) :
x = y
@[ext]
structure nonempty_interval (α : Type u_6) [has_le α] :
Type u_6

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_6} {_inst_1 : has_le α} (x y : nonempty_interval α) :

The injection that induces the order on intervals.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

to_dual_prod as an order embedding.

Equations

Turn an interval into an interval in the dual order.

Equations
@[simp]
theorem nonempty_interval.pure_to_prod {α : Type u_1} [preorder α] (a : α) :
def nonempty_interval.pure {α : Type u_1} [preorder α] (a : α) :

{a} as an interval.

Equations
@[protected, instance]
@[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 α) :
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations
@[simp]
theorem nonempty_interval.mem_mk {α : Type u_1} [partial_order α] {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} [partial_order α] {s : nonempty_interval α} {a : α} :
@[simp, norm_cast]
theorem nonempty_interval.coe_subset_coe {α : Type u_1} [partial_order α] {s t : nonempty_interval α} :
s t s t
@[simp, norm_cast]
theorem nonempty_interval.coe_ssubset_coe {α : Type u_1} [partial_order α] {s t : nonempty_interval α} :
s t s < t
@[simp, norm_cast]
theorem nonempty_interval.coe_pure {α : Type u_1} [partial_order α] (s : α) :
@[simp, norm_cast]
@[protected, instance]
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]
Equations
@[protected, instance]
def interval.can_lift {α : Type u_1} [has_le α] :
Equations
@[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 : interval α Prop} :
( (s : interval α), p s) p (s : nonempty_interval α), p s
@[protected]
theorem interval.exists {α : Type u_1} [has_le α] {p : interval α Prop} :
( (s : interval α), p s) p (s : nonempty_interval α), 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
@[simp]
theorem interval.dual_bot {α : Type u_1} [preorder α] :
@[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 α) :
@[simp]
theorem interval.dual_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (s : interval α) :
@[simp]
def interval.coe_hom {α : Type u_1} [partial_order α] :

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

Equations
@[protected, instance]
def interval.set_like {α : Type u_1} [partial_order α] :
Equations
@[simp, norm_cast]
theorem interval.coe_subset_coe {α : Type u_1} [partial_order α] {s t : interval α} :
s t s t
@[simp, norm_cast]
theorem interval.coe_ssubset_coe {α : Type u_1} [partial_order α] {s t : interval α} :
s t s < t
@[simp, norm_cast]
theorem interval.coe_pure {α : Type u_1} [partial_order α] (a : α) :
@[simp, norm_cast]
theorem interval.coe_coe {α : Type u_1} [partial_order α] (s : nonempty_interval α) :
@[simp, norm_cast]
theorem interval.coe_bot {α : Type u_1} [partial_order α] :
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[simp, norm_cast]
theorem interval.coe_inf {α : Type u_1} [lattice α] [decidable_rel has_le.le] (s t : interval α) :
(s t) = s t
@[simp, norm_cast]
theorem interval.disjoint_coe {α : Type u_1} [lattice α] (s t : interval α) :
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem nonempty_interval.mem_coe_interval {α : Type u_1} [partial_order α] {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]
Equations
@[simp, norm_cast]
theorem interval.coe_Inf {α : Type u_1} [complete_lattice α] (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_4} [complete_lattice α] (f : ι interval α) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem interval.coe_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [complete_lattice α] (f : Π (i : ι), κ i interval α) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)