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 Prod :

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

source

theorem NonemptyInterval.toProd_injective {α : Type u_1} [LE α] :

Function.Injective NonemptyInterval.toProd

source

theorem NonemptyInterval.ext {α : Type u_1} [LE α] (s : NonemptyInterval α) (t : NonemptyInterval α) (h : s.toProd = t.toProd) :

s = t

source

theorem NonemptyInterval.ext_iff {α : Type u_1} [LE α] (s : NonemptyInterval α) (t : NonemptyInterval α) :

s = t ↔ s.toProd = t.toProd

source

def NonemptyInterval.toDualProd {α : Type u_1} [LE α] :

NonemptyInterval α → αᵒᵈ × α

The injection that induces the order on intervals.

Instances For

source

@[simp]

theorem NonemptyInterval.toDualProd_apply {α : Type u_1} [LE α] (s : NonemptyInterval α) :

NonemptyInterval.toDualProd s = (↑OrderDual.toDual s.fst, s.snd)

source

theorem NonemptyInterval.toDualProd_injective {α : Type u_1} [LE α] :

Function.Injective NonemptyInterval.toDualProd

source

instance NonemptyInterval.instIsEmptyNonemptyInterval {α : Type u_1} [LE α] [IsEmpty α] :

IsEmpty (NonemptyInterval α)

source

instance NonemptyInterval.instSubsingletonNonemptyInterval {α : Type u_1} [LE α] [Subsingleton α] :

Subsingleton (NonemptyInterval α)

source

instance NonemptyInterval.le {α : Type u_1} [LE α] :

LE (NonemptyInterval α)

source

theorem NonemptyInterval.le_def {α : Type u_1} [LE α] {s : NonemptyInterval α} {t : NonemptyInterval α} :

s ≤ t ↔ t.fst ≤ s.fst ∧ s.snd ≤ t.snd

source

@[simp]

theorem NonemptyInterval.toDualProdHom_apply {α : Type u_1} [LE α] :

∀ (a : NonemptyInterval α), ↑NonemptyInterval.toDualProdHom a = NonemptyInterval.toDualProd a

source

def NonemptyInterval.toDualProdHom {α : Type u_1} [LE α] :

NonemptyInterval α ↪o αᵒᵈ × α

toDualProd as an order embedding.

Instances For

source

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

NonemptyInterval α ≃ NonemptyInterval αᵒᵈ

Turn an interval into an interval in the dual order.

Instances For

source

@[simp]

theorem NonemptyInterval.fst_dual {α : Type u_1} [LE α] (s : NonemptyInterval α) :

(↑NonemptyInterval.dual s).fst = ↑OrderDual.toDual s.snd

source

@[simp]

theorem NonemptyInterval.snd_dual {α : Type u_1} [LE α] (s : NonemptyInterval α) :

(↑NonemptyInterval.dual s).snd = ↑OrderDual.toDual s.fst

source

instance NonemptyInterval.instPreorderNonemptyIntervalToLE {α : Type u_1} [Preorder α] :

Preorder (NonemptyInterval α)

source

instance NonemptyInterval.instCoeNonemptyIntervalToLESet {α : Type u_1} [Preorder α] :

Coe (NonemptyInterval α) (Set α)

source

instance NonemptyInterval.instMembershipNonemptyIntervalToLE {α : Type u_1} [Preorder α] :

Membership α (NonemptyInterval α)

source

@[simp]

theorem NonemptyInterval.mem_mk {α : Type u_1} [Preorder α] {x : α × α} {a : α} {hx : x.fst ≤ x.snd} :

a ∈ { toProd := x, fst_le_snd := hx } ↔ x.fst ≤ a ∧ a ≤ x.snd

source

theorem NonemptyInterval.mem_def {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} :

a ∈ s ↔ s.fst ≤ a ∧ a ≤ s.snd

source

theorem NonemptyInterval.coe_nonempty {α : Type u_1} [Preorder α] (s : NonemptyInterval α) :

Set.Nonempty (Set.Icc s.fst s.snd)

source

@[simp]

theorem NonemptyInterval.pure_fst {α : Type u_1} [Preorder α] (a : α) :

(NonemptyInterval.pure a).toProd.fst = a

source

@[simp]

theorem NonemptyInterval.pure_snd {α : Type u_1} [Preorder α] (a : α) :

(NonemptyInterval.pure a).toProd.snd = a

source

def NonemptyInterval.pure {α : Type u_1} [Preorder α] (a : α) :

NonemptyInterval α

{a} as an interval.

Instances For

source

theorem NonemptyInterval.mem_pure_self {α : Type u_1} [Preorder α] (a : α) :

a ∈ NonemptyInterval.pure a

source

theorem NonemptyInterval.pure_injective {α : Type u_1} [Preorder α] :

Function.Injective NonemptyInterval.pure

source

@[simp]

theorem NonemptyInterval.dual_pure {α : Type u_1} [Preorder α] (a : α) :

↑NonemptyInterval.dual (NonemptyInterval.pure a) = NonemptyInterval.pure (↑OrderDual.toDual a)

source

instance NonemptyInterval.instInhabitedNonemptyIntervalToLE {α : Type u_1} [Preorder α] [Inhabited α] :

Inhabited (NonemptyInterval α)

source

instance NonemptyInterval.instNonemptyNonemptyIntervalToLE {α : Type u_1} [Preorder α] [Nonempty α] :

Nonempty (NonemptyInterval α)

source

instance NonemptyInterval.instNontrivialNonemptyIntervalToLE {α : Type u_1} [Preorder α] [Nontrivial α] :

Nontrivial (NonemptyInterval α)

source

@[simp]

theorem NonemptyInterval.map_snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :

(NonemptyInterval.map f a).toProd.snd = ↑f a.1.snd

source

@[simp]

theorem NonemptyInterval.map_fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :

(NonemptyInterval.map f a).toProd.fst = ↑f a.1.fst

source

def NonemptyInterval.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :

NonemptyInterval β

Pushforward of nonempty intervals.

Instances For

source

@[simp]

theorem NonemptyInterval.map_pure {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : α) :

NonemptyInterval.map f (NonemptyInterval.pure a) = NonemptyInterval.pure (↑f a)

source

@[simp]

theorem NonemptyInterval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) (a : NonemptyInterval α) :

NonemptyInterval.map g (NonemptyInterval.map f a) = NonemptyInterval.map (OrderHom.comp g f) a

source

@[simp]

theorem NonemptyInterval.dual_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :

↑NonemptyInterval.dual (NonemptyInterval.map f a) = NonemptyInterval.map (↑OrderHom.dual f) (↑NonemptyInterval.dual a)

source

@[simp]

theorem NonemptyInterval.map₂_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :

∀ (a : NonemptyInterval α) (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.snd = f a.snd a_1.snd

source

@[simp]

theorem NonemptyInterval.map₂_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :

∀ (a : NonemptyInterval α) (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.fst = f a.fst a_1.fst

source

def NonemptyInterval.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :

NonemptyInterval α → NonemptyInterval β → NonemptyInterval γ

Binary pushforward of nonempty intervals.

Instances For

source

@[simp]

theorem NonemptyInterval.map₂_pure {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (a : α) (b : β) :

NonemptyInterval.map₂ f h₀ h₁ (NonemptyInterval.pure a) (NonemptyInterval.pure b) = NonemptyInterval.pure (f a b)

source

@[simp]

theorem NonemptyInterval.dual_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (s : NonemptyInterval α) (t : NonemptyInterval β) :

↑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)

source

instance NonemptyInterval.instOrderTopNonemptyIntervalToLELe {α : Type u_1} [Preorder α] [BoundedOrder α] :

OrderTop (NonemptyInterval α)

source

@[simp]

theorem NonemptyInterval.dual_top {α : Type u_1} [Preorder α] [BoundedOrder α] :

↑NonemptyInterval.dual ⊤ = ⊤

source

instance NonemptyInterval.instPartialOrderNonemptyIntervalToLEToPreorder {α : Type u_1} [PartialOrder α] :

PartialOrder (NonemptyInterval α)

source

def NonemptyInterval.coeHom {α : Type u_1} [PartialOrder α] :

NonemptyInterval α ↪o Set α

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

Instances For

source

instance NonemptyInterval.setLike {α : Type u_1} [PartialOrder α] :

SetLike (NonemptyInterval α) α

source

theorem NonemptyInterval.coe_subset_coe {α : Type u_1} [PartialOrder α] {s : NonemptyInterval α} {t : NonemptyInterval α} :

↑s ⊆ ↑t ↔ s ≤ t

source

theorem NonemptyInterval.coe_ssubset_coe {α : Type u_1} [PartialOrder α] {s : NonemptyInterval α} {t : NonemptyInterval α} :

↑s ⊂ ↑t ↔ s < t

source

@[simp]

theorem NonemptyInterval.coe_coeHom {α : Type u_1} [PartialOrder α] :

↑NonemptyInterval.coeHom = SetLike.coe

source

@[simp]

theorem NonemptyInterval.coe_pure {α : Type u_1} [PartialOrder α] (a : α) :

↑(NonemptyInterval.pure a) = {a}

source

@[simp]

theorem NonemptyInterval.mem_pure {α : Type u_1} [PartialOrder α] {a : α} {b : α} :

b ∈ NonemptyInterval.pure a ↔ b = a

source

@[simp]

theorem NonemptyInterval.coe_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] :

↑⊤ = Set.univ

source

@[simp]

theorem NonemptyInterval.coe_dual {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) :

↑(↑NonemptyInterval.dual s) = ↑OrderDual.ofDual ⁻¹' ↑s

source

theorem NonemptyInterval.subset_coe_map {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α →o β) (s : NonemptyInterval α) :

↑f '' ↑s ⊆ ↑(NonemptyInterval.map f s)

source

instance NonemptyInterval.instSupNonemptyIntervalToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [Lattice α] :

Sup (NonemptyInterval α)

source

instance NonemptyInterval.instSemilatticeSupNonemptyIntervalToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [Lattice α] :

SemilatticeSup (NonemptyInterval α)

source

@[simp]

theorem NonemptyInterval.fst_sup {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (t : NonemptyInterval α) :

(s ⊔ t).fst = s.fst ⊓ t.fst

source

@[simp]

theorem NonemptyInterval.snd_sup {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (t : NonemptyInterval α) :

(s ⊔ t).snd = s.snd ⊔ t.snd

source

@[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

source

instance Interval.instInhabitedInterval {α : Type u_1} [LE α] :

Inhabited (Interval α)

source

instance Interval.instLEInterval {α : Type u_1} [LE α] :

LE (Interval α)

source

instance Interval.instOrderBotIntervalInstLEInterval {α : Type u_1} [LE α] :

OrderBot (Interval α)

source

instance Interval.instCoeNonemptyIntervalInterval {α : Type u_1} [LE α] :

Coe (NonemptyInterval α) (Interval α)

source

instance Interval.canLift {α : Type u_1} [LE α] :

CanLift (Interval α) (NonemptyInterval α) WithBot.some fun r => r ≠ ⊥

source

theorem Interval.coe_injective {α : Type u_1} [LE α] :

Function.Injective WithBot.some

source

theorem Interval.coe_inj {α : Type u_1} [LE α] {s : NonemptyInterval α} {t : NonemptyInterval α} :

↑s = ↑t ↔ s = t

source

theorem Interval.forall {α : Type u_1} [LE α] {p : Interval α → Prop} :

((s : Interval α) → p s) ↔ p ⊥ ∧ ((s : NonemptyInterval α) → p ↑s)

source

theorem Interval.exists {α : Type u_1} [LE α] {p : Interval α → Prop} :

(∃ s, p s) ↔ p ⊥ ∨ ∃ s, p ↑s

source

instance Interval.instUniqueInterval {α : Type u_1} [LE α] [IsEmpty α] :

Unique (Interval α)

source

def Interval.dual {α : Type u_1} [LE α] :

Interval α ≃ Interval αᵒᵈ

Turn an interval into an interval in the dual order.

Instances For

source

instance Interval.instPreorderIntervalToLE {α : Type u_1} [Preorder α] :

Preorder (Interval α)

source

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

Interval α

{a} as an interval.

Instances For

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 (↑OrderDual.toDual 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

instance Interval.instNontrivialIntervalToLE {α : 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.

Instances For

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 (OrderHom.comp g 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 (↑OrderHom.dual f) (↑Interval.dual s)

source

instance Interval.boundedOrder {α : Type u_1} [Preorder α] [BoundedOrder α] :

BoundedOrder (Interval α)

source

@[simp]

theorem Interval.dual_top {α : Type u_1} [Preorder α] [BoundedOrder α] :

↑Interval.dual ⊤ = ⊤

source

instance Interval.partialOrder {α : Type u_1} [PartialOrder α] :

PartialOrder (Interval α)

source

def Interval.coeHom {α : Type u_1} [PartialOrder α] :

Interval α ↪o Set α

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

Instances For

source

instance Interval.setLike {α : Type u_1} [PartialOrder α] :

SetLike (Interval α) α

source

theorem Interval.coe_subset_coe {α : Type u_1} [PartialOrder α] {s : Interval α} {t : Interval α} :

↑s ⊆ ↑t ↔ s ≤ t

source

theorem Interval.coe_sSubset_coe {α : Type u_1} [PartialOrder α] {s : Interval α} {t : Interval α} :

↑s ⊂ ↑t ↔ s < t

source

@[simp]

theorem Interval.coe_pure {α : Type u_1} [PartialOrder α] (a : α) :

↑(Interval.pure a) = {a}

source

@[simp]

theorem Interval.coe_coe {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) :

↑↑s = ↑s

source

@[simp]

theorem Interval.coe_bot {α : Type u_1} [PartialOrder α] :

↑⊥ = ∅

source

@[simp]

theorem Interval.coe_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] :

↑⊤ = Set.univ

source

@[simp]

theorem Interval.coe_dual {α : Type u_1} [PartialOrder α] (s : Interval α) :

↑(↑Interval.dual s) = ↑OrderDual.ofDual ⁻¹' ↑s

source

theorem Interval.subset_coe_map {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α →o β) (s : Interval α) :

↑f '' ↑s ⊆ ↑(Interval.map f s)

source

@[simp]

theorem Interval.mem_pure {α : Type u_1} [PartialOrder α] {a : α} {b : α} :

b ∈ Interval.pure a ↔ b = a

source

theorem Interval.mem_pure_self {α : Type u_1} [PartialOrder α] (a : α) :

a ∈ Interval.pure a

source

instance Interval.semilatticeSup {α : Type u_1} [Lattice α] :

SemilatticeSup (Interval α)

source

instance Interval.lattice {α : Type u_1} [Lattice α] [DecidableRel fun x x_1 => x ≤ x_1] :

Lattice (Interval α)

source

@[simp]

theorem Interval.coe_inf {α : Type u_1} [Lattice α] [DecidableRel fun x x_1 => x ≤ x_1] (s : Interval α) (t : Interval α) :

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

theorem Interval.disjoint_coe {α : Type u_1} [Lattice α] (s : Interval α) (t : Interval α) :

Disjoint ↑s ↑t ↔ Disjoint s t

source

@[simp]

theorem NonemptyInterval.coe_pure_interval {α : Type u_1} [Preorder α] (a : α) :

↑(NonemptyInterval.pure a) = Interval.pure a

source

@[simp]

theorem NonemptyInterval.coe_eq_pure {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} :

↑s = Interval.pure a ↔ s = NonemptyInterval.pure a

source

@[simp]

theorem NonemptyInterval.coe_top_interval {α : Type u_1} [Preorder α] [BoundedOrder α] :

↑⊤ = ⊤

source

@[simp]

theorem NonemptyInterval.mem_coe_interval {α : Type u_1} [PartialOrder α] {s : NonemptyInterval α} {x : α} :

x ∈ ↑s ↔ x ∈ s

source

@[simp]

theorem NonemptyInterval.coe_sup_interval {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (t : NonemptyInterval α) :

↑(s ⊔ t) = ↑s ⊔ ↑t

source

noncomputable instance Interval.completeLattice {α : Type u_1} [CompleteLattice α] [DecidableRel fun x x_1 => x ≤ x_1] :

CompleteLattice (Interval α)

source

@[simp]

theorem Interval.coe_sInf {α : Type u_1} [CompleteLattice α] [DecidableRel fun x x_1 => x ≤ x_1] (S : Set (Interval α)) :

↑(sInf S) = ⋂ (s : Interval α) (_ : s ∈ S), ↑s

source

@[simp]

theorem Interval.coe_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [DecidableRel fun x x_1 => x ≤ x_1] (f : ι → Interval α) :

↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

source

theorem Interval.coe_iInf₂ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_6} [CompleteLattice α] [DecidableRel fun x x_1 => x ≤ x_1] (f : (i : ι) → κ i → Interval α) :

↑(⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)