mathlib3 documentation

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 #

theorem nonempty_interval.ext {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) (h : x.to_prod = y.to_prod) :
x = y
theorem nonempty_interval.ext_iff {α : Type u_7} {_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
@[protected, instance]
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]
@[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 α) :
@[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 β) :
(nonempty_interval.map₂ f h₀ 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]
Equations
@[protected, instance]
Equations

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

Equations
@[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 α] (a : α) :
@[simp]
theorem nonempty_interval.mem_pure {α : Type u_1} [partial_order α] {a b : α} :
@[simp, norm_cast]
theorem nonempty_interval.subset_coe_map {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : α →o β) (s : nonempty_interval α) :
@[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 α] :
@[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 α] :
@[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 α) :
@[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]
theorem interval.subset_coe_map {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : α →o β) (s : interval α) :
@[simp]
theorem interval.mem_pure {α : Type u_1} [partial_order α] {a b : α} :
theorem interval.mem_pure_self {α : Type u_1} [partial_order α] (a : α) :
@[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]
@[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 α] [decidable_rel has_le.le] (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} [complete_lattice α] [decidable_rel has_le.le] (f : ι interval α) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem interval.coe_infi₂ {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_6} [complete_lattice α] [decidable_rel has_le.le] (f : Π (i : ι), κ i interval α) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)