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 #

source
theorem nonempty_interval.ext {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) (h : x.to_prod = y.to_prod) :
x = y
source
@[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
source
theorem nonempty_interval.ext_iff {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) :
x = y ↔ x.to_prod = y.to_prod
source
theorem nonempty_interval.to_prod_injective {α : Type u_1} [has_le α] :
function.injective nonempty_interval.to_prod
source
def nonempty_interval.to_dual_prod {α : Type u_1} [has_le α] :
nonempty_interval α → αᵒᵈ × α

The injection that induces the order on intervals.

Equations
source
@[simp]
theorem nonempty_interval.to_dual_prod_apply {α : Type u_1} [has_le α] (s : nonempty_interval α) :
s.to_dual_prod = (⇑order_dual.to_dual s.to_prod.fst, s.to_prod.snd)
source
theorem nonempty_interval.to_dual_prod_injective {α : Type u_1} [has_le α] :
function.injective nonempty_interval.to_dual_prod
source
@[protected, instance]
def nonempty_interval.is_empty {α : Type u_1} [has_le α] [is_empty α] :
is_empty (nonempty_interval α)
source
@[protected, instance]
def nonempty_interval.subsingleton {α : Type u_1} [has_le α] [subsingleton α] :
subsingleton (nonempty_interval α)
source
@[protected, instance]
def nonempty_interval.has_le {α : Type u_1} [has_le α] :
has_le (nonempty_interval α)
Equations
source
theorem nonempty_interval.le_def {α : Type u_1} [has_le α] {s t : nonempty_interval α} :
s ≤ t ↔ t.to_prod.fst ≤ s.to_prod.fst ∧ s.to_prod.snd ≤ t.to_prod.snd
source
def nonempty_interval.to_dual_prod_hom {α : Type u_1} [has_le α] :
nonempty_interval α ↪o αᵒᵈ × α

to_dual_prod as an order embedding.

Equations
source
@[simp]
theorem nonempty_interval.to_dual_prod_hom_apply {α : Type u_1} [has_le α] (ᾰ : nonempty_interval α) :
⇑nonempty_interval.to_dual_prod_hom ᾰ = ᾰ.to_dual_prod
source
def nonempty_interval.dual {α : Type u_1} [has_le α] :
nonempty_interval α ≃ nonempty_interval αᵒᵈ

Turn an interval into an interval in the dual order.

Equations
source
@[simp]
theorem nonempty_interval.fst_dual {α : Type u_1} [has_le α] (s : nonempty_interval α) :
(⇑nonempty_interval.dual s).to_prod.fst = ⇑order_dual.to_dual s.to_prod.snd
source
@[simp]
theorem nonempty_interval.snd_dual {α : Type u_1} [has_le α] (s : nonempty_interval α) :
(⇑nonempty_interval.dual s).to_prod.snd = ⇑order_dual.to_dual s.to_prod.fst
source
@[protected, instance]
def nonempty_interval.preorder {α : Type u_1} [preorder α] :
preorder (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.set.has_coe_t {α : Type u_1} [preorder α] :
has_coe_t (nonempty_interval α) (set α)
Equations
source
@[protected, instance]
def nonempty_interval.has_mem {α : Type u_1} [preorder α] :
has_mem α (nonempty_interval α)
Equations
source
@[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
source
theorem nonempty_interval.mem_def {α : Type u_1} [preorder α] {s : nonempty_interval α} {a : α} :
a ∈ s ↔ s.to_prod.fst ≤ a ∧ a ≤ s.to_prod.snd
source
@[simp]
theorem nonempty_interval.coe_nonempty {α : Type u_1} [preorder α] (s : nonempty_interval α) :
↑s.nonempty
source
@[simp]
theorem nonempty_interval.pure_to_prod {α : Type u_1} [preorder α] (a : α) :
(nonempty_interval.pure a).to_prod = (a, a)
source
def nonempty_interval.pure {α : Type u_1} [preorder α] (a : α) :
nonempty_interval α

{a} as an interval.

Equations
source
theorem nonempty_interval.mem_pure_self {α : Type u_1} [preorder α] (a : α) :
a ∈ nonempty_interval.pure a
source
theorem nonempty_interval.pure_injective {α : Type u_1} [preorder α] :
function.injective nonempty_interval.pure
source
@[simp]
theorem nonempty_interval.dual_pure {α : Type u_1} [preorder α] (a : α) :
⇑nonempty_interval.dual (nonempty_interval.pure a) = nonempty_interval.pure (⇑order_dual.to_dual a)
source
@[protected, instance]
def nonempty_interval.inhabited {α : Type u_1} [preorder α] [inhabited α] :
inhabited (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.nonempty {α : Type u_1} [preorder α] [nonempty α] :
nonempty (nonempty_interval α)
source
@[protected, instance]
def nonempty_interval.nontrivial {α : Type u_1} [preorder α] [nontrivial α] :
nontrivial (nonempty_interval α)
source
@[simp]
theorem nonempty_interval.map_to_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :
(nonempty_interval.map f a).to_prod = prod.map ⇑f ⇑f a.to_prod
source
def nonempty_interval.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :
nonempty_interval β

Pushforward of nonempty intervals.

Equations
source
@[simp]
theorem nonempty_interval.map_pure {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : α) :
nonempty_interval.map f (nonempty_interval.pure a) = nonempty_interval.pure (⇑f a)
source
@[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 α) :
nonempty_interval.map g (nonempty_interval.map f a) = nonempty_interval.map (g.comp f) a
source
@[simp]
theorem nonempty_interval.dual_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :
⇑nonempty_interval.dual (nonempty_interval.map f a) = nonempty_interval.map (⇑order_hom.dual f) (⇑nonempty_interval.dual a)
source
@[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)
source
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)) :
nonempty_interval α → nonempty_interval β → nonempty_interval γ

Binary pushforward of nonempty intervals.

Equations
source
@[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 : β) :
nonempty_interval.map₂ f h₀ h₁ (nonempty_interval.pure a) (nonempty_interval.pure b) = nonempty_interval.pure (f a b)
source
@[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 β) :
⇑nonempty_interval.dual (nonempty_interval.map₂ f h₀ h₁ s t) = nonempty_interval.map₂ (λ (a : αᵒᵈ) (b : βᵒᵈ), ⇑order_dual.to_dual (f (⇑order_dual.of_dual a) (⇑order_dual.of_dual b))) _ _ (⇑nonempty_interval.dual s) (⇑nonempty_interval.dual t)
source
@[protected, instance]
def nonempty_interval.order_top {α : Type u_1} [preorder α] [bounded_order α] :
order_top (nonempty_interval α)
Equations
source
@[simp]
theorem nonempty_interval.dual_top {α : Type u_1} [preorder α] [bounded_order α] :
⇑nonempty_interval.dual ⊤ = ⊤
source
@[protected, instance]
def nonempty_interval.partial_order {α : Type u_1} [partial_order α] :
partial_order (nonempty_interval α)
Equations
source
def nonempty_interval.coe_hom {α : Type u_1} [partial_order α] :
nonempty_interval α ↪o set α

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

Equations
source
@[protected, instance]
def nonempty_interval.set_like {α : Type u_1} [partial_order α] :
set_like (nonempty_interval α) α
Equations
source
@[simp, norm_cast]
theorem nonempty_interval.coe_subset_coe {α : Type u_1} [partial_order α] {s t : nonempty_interval α} :
↑s ⊆ ↑t ↔ s ≤ t
source
@[simp, norm_cast]
theorem nonempty_interval.coe_ssubset_coe {α : Type u_1} [partial_order α] {s t : nonempty_interval α} :
↑s ⊂ ↑t ↔ s < t
source
@[simp]
theorem nonempty_interval.coe_coe_hom {α : Type u_1} [partial_order α] :
⇑nonempty_interval.coe_hom = coe
source
@[simp, norm_cast]
theorem nonempty_interval.coe_pure {α : Type u_1} [partial_order α] (a : α) :
↑(nonempty_interval.pure a) = {a}
source
@[simp]
theorem nonempty_interval.mem_pure {α : Type u_1} [partial_order α] {a b : α} :
b ∈ nonempty_interval.pure a ↔ b = a
source
@[simp, norm_cast]
theorem nonempty_interval.coe_top {α : Type u_1} [partial_order α] [bounded_order α] :
↑⊤ = set.univ
source
@[simp, norm_cast]
theorem nonempty_interval.coe_dual {α : Type u_1} [partial_order α] (s : nonempty_interval α) :
↑(⇑nonempty_interval.dual s) = ⇑order_dual.of_dual ⁻¹' ↑s
source
theorem nonempty_interval.subset_coe_map {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : α →o β) (s : nonempty_interval α) :
⇑f '' ↑s ⊆ ↑(nonempty_interval.map f s)
source
@[protected, instance]
def nonempty_interval.has_sup {α : Type u_1} [lattice α] :
has_sup (nonempty_interval α)
Equations
source
@[protected, instance]
def nonempty_interval.semilattice_sup {α : Type u_1} [lattice α] :
semilattice_sup (nonempty_interval α)
Equations
source
@[simp]
theorem nonempty_interval.fst_sup {α : Type u_1} [lattice α] (s t : nonempty_interval α) :
(s ⊔ t).to_prod.fst = s.to_prod.fst ⊓ t.to_prod.fst
source
@[simp]
theorem nonempty_interval.snd_sup {α : Type u_1} [lattice α] (s t : nonempty_interval α) :
(s ⊔ t).to_prod.snd = s.to_prod.snd ⊔ t.to_prod.snd
source
@[protected, instance]
def interval.has_le (α : Type u_1) [has_le α] :
has_le (interval α)
source
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
source
@[protected, instance]
def interval.inhabited (α : Type u_1) [has_le α] :
inhabited (interval α)
source
@[protected, instance]
def interval.order_bot (α : Type u_1) [has_le α] :
order_bot (interval α)
source
@[protected, instance]
def interval.has_coe_t {α : Type u_1} [has_le α] :
has_coe_t (nonempty_interval α) (interval α)
Equations
source
@[protected, instance]
def interval.can_lift {α : Type u_1} [has_le α] :
can_lift (interval α) (nonempty_interval α) coe (λ (r : interval α), r ≠ ⊥)
Equations
source
theorem interval.coe_injective {α : Type u_1} [has_le α] :
function.injective coe
source
@[simp, norm_cast]
theorem interval.coe_inj {α : Type u_1} [has_le α] {s t : nonempty_interval α} :
↑s = ↑t ↔ s = t
source
@[protected]
theorem interval.forall {α : Type u_1} [has_le α] {p : interval α → Prop} :
(∀ (s : interval α), p s) ↔ p ⊥ ∧ ∀ (s : nonempty_interval α), p ↑s
source
@[protected]
theorem interval.exists {α : Type u_1} [has_le α] {p : interval α → Prop} :
(∃ (s : interval α), p s) ↔ p ⊥ ∨ ∃ (s : nonempty_interval α), p ↑s
source
@[protected, instance]
def interval.unique {α : Type u_1} [has_le α] [is_empty α] :
unique (interval α)
Equations
source
def interval.dual {α : Type u_1} [has_le α] :
interval α ≃ interval αᵒᵈ

Turn an interval into an interval in the dual order.

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

{a} as an interval.

Equations
source
theorem interval.pure_injective {α : Type u_1} [preorder α] :
function.injective interval.pure
source
@[simp]
theorem interval.dual_pure {α : Type u_1} [preorder α] (a : α) :
⇑interval.dual (interval.pure a) = interval.pure (⇑order_dual.to_dual a)
source
@[simp]
theorem interval.dual_bot {α : Type u_1} [preorder α] :
⇑interval.dual ⊥ = ⊥
source
@[simp]
theorem interval.pure_ne_bot {α : Type u_1} [preorder α] {a : α} :
interval.pure a ≠ ⊥
source
@[simp]
theorem interval.bot_ne_pure {α : Type u_1} [preorder α] {a : α} :
⊥ ≠ interval.pure a
source
@[protected, instance]
def interval.nontrivial {α : Type u_1} [preorder α] [nonempty α] :
nontrivial (interval α)
source
def interval.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) :
interval α → interval β

Pushforward of intervals.

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

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

Equations
source
@[protected, instance]
def interval.set_like {α : Type u_1} [partial_order α] :
set_like (interval α) α
Equations
source
@[simp, norm_cast]
theorem interval.coe_subset_coe {α : Type u_1} [partial_order α] {s t : interval α} :
↑s ⊆ ↑t ↔ s ≤ t
source
@[simp, norm_cast]
theorem interval.coe_ssubset_coe {α : Type u_1} [partial_order α] {s t : interval α} :
↑s ⊂ ↑t ↔ s < t
source
@[simp, norm_cast]
theorem interval.coe_pure {α : Type u_1} [partial_order α] (a : α) :
↑(interval.pure a) = {a}
source
@[simp, norm_cast]
theorem interval.coe_coe {α : Type u_1} [partial_order α] (s : nonempty_interval α) :
↑↑s = ↑s
source
@[simp, norm_cast]
theorem interval.coe_bot {α : Type u_1} [partial_order α] :
↑⊥ = ∅
source
@[simp, norm_cast]
theorem interval.coe_top {α : Type u_1} [partial_order α] [bounded_order α] :
↑⊤ = set.univ
source
@[simp, norm_cast]
theorem interval.coe_dual {α : Type u_1} [partial_order α] (s : interval α) :
↑(⇑interval.dual s) = ⇑order_dual.of_dual ⁻¹' ↑s
source
theorem interval.subset_coe_map {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] (f : α →o β) (s : interval α) :
⇑f '' ↑s ⊆ ↑(interval.map f s)
source
@[simp]
theorem interval.mem_pure {α : Type u_1} [partial_order α] {a b : α} :
b ∈ interval.pure a ↔ b = a
source
theorem interval.mem_pure_self {α : Type u_1} [partial_order α] (a : α) :
a ∈ interval.pure a
source
@[protected, instance]
def interval.semilattice_sup {α : Type u_1} [lattice α] :
semilattice_sup (interval α)
Equations
source
@[protected, instance]
def interval.lattice {α : Type u_1} [lattice α] [decidable_rel has_le.le] :
lattice (interval α)
Equations
source
@[simp, norm_cast]
theorem interval.coe_inf {α : Type u_1} [lattice α] [decidable_rel has_le.le] (s t : interval α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp, norm_cast]
theorem interval.disjoint_coe {α : Type u_1} [lattice α] (s t : interval α) :
disjoint ↑s ↑t ↔ disjoint s t
source
@[simp, norm_cast]
theorem nonempty_interval.coe_pure_interval {α : Type u_1} [preorder α] (a : α) :
↑(nonempty_interval.pure a) = interval.pure a
source
@[simp, norm_cast]
theorem nonempty_interval.coe_eq_pure {α : Type u_1} [preorder α] {s : nonempty_interval α} {a : α} :
↑s = interval.pure a ↔ s = nonempty_interval.pure a
source
@[simp, norm_cast]
theorem nonempty_interval.coe_top_interval {α : Type u_1} [preorder α] [bounded_order α] :
↑⊤ = ⊤
source
@[simp, norm_cast]
theorem nonempty_interval.mem_coe_interval {α : Type u_1} [partial_order α] {s : nonempty_interval α} {x : α} :
x ∈ ↑s ↔ x ∈ s
source
@[simp, norm_cast]
theorem nonempty_interval.coe_sup_interval {α : Type u_1} [lattice α] (s t : nonempty_interval α) :
↑(s ⊔ t) = ↑s ⊔ ↑t
source
@[protected, instance]
noncomputable def interval.complete_lattice {α : Type u_1} [complete_lattice α] [decidable_rel has_le.le] :
complete_lattice (interval α)
Equations
source
@[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
source
@[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)
source
@[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)