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_6) [LE α] extends α × α : 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 NonemptyInterval α → Set α.

• fst : α
• snd : α
• fst_le_snd : self.toProd.1 ≤ self.toProd.2

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

theorem NonemptyInterval.ext_iff {α : Type u_6} {inst✝ : LE α} {x y : NonemptyInterval α} : x = y ↔ x.toProd = y.toProd

theorem NonemptyInterval.ext {α : Type u_6} {inst✝ : LE α} {x y : NonemptyInterval α} (toProd : x.toProd = y.toProd) : x = y

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

instance NonemptyInterval.instCanLift {α : Type u_1} [LE α] : CanLift (α × α) (NonemptyInterval α) toProd fun (x : α × α) => x.1 ≤ x.2

Allow lifting a pair (a, b) with a ≤ b to NonemptyInterval in the lift tactic.

def NonemptyInterval.toDualProd {α : Type u_1} [LE α] : NonemptyInterval α → αᵒᵈ × α

The injection that induces the order on intervals.

@[simp]

theorem NonemptyInterval.toDualProd_apply {α : Type u_1} [LE α] (s : NonemptyInterval α) : s.toDualProd = (OrderDual.toDual s.toProd.1, s.toProd.2)

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

instance NonemptyInterval.instIsEmpty {α : Type u_1} [LE α] [IsEmpty α] : IsEmpty (NonemptyInterval α)

instance NonemptyInterval.instSubsingleton {α : Type u_1} [LE α] [Subsingleton α] : Subsingleton (NonemptyInterval α)

@[implicit_reducible]

instance NonemptyInterval.instDecidableEq {α : Type u_1} [LE α] [DecidableEq α] : DecidableEq (NonemptyInterval α)

@[implicit_reducible]

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

theorem NonemptyInterval.le_def {α : Type u_1} [LE α] {s t : NonemptyInterval α} : s ≤ t ↔ t.toProd.1 ≤ s.toProd.1 ∧ s.toProd.2 ≤ t.toProd.2

@[implicit_reducible]

instance NonemptyInterval.instDecidableLE {α : Type u_1} [LE α] [DecidableLE α] : DecidableLE (NonemptyInterval α)

def NonemptyInterval.toDualProdHom {α : Type u_1} [LE α] : NonemptyInterval α ↪o αᵒᵈ × α

toDualProd as an order embedding.

@[simp]

theorem NonemptyInterval.toDualProdHom_apply {α : Type u_1} [LE α] (a✝ : NonemptyInterval α) : toDualProdHom a✝ = a✝.toDualProd

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

Turn an interval into an interval in the dual order.

@[simp]

theorem NonemptyInterval.fst_dual {α : Type u_1} [LE α] (s : NonemptyInterval α) : (dual s).toProd.1 = OrderDual.toDual s.toProd.2

@[simp]

theorem NonemptyInterval.snd_dual {α : Type u_1} [LE α] (s : NonemptyInterval α) : (dual s).toProd.2 = OrderDual.toDual s.toProd.1

@[implicit_reducible]

instance NonemptyInterval.instPreorder {α : Type u_1} [Preorder α] : Preorder (NonemptyInterval α)

theorem NonemptyInterval.toDualProd_mono {α : Type u_1} [Preorder α] : Monotone toDualProd

theorem NonemptyInterval.toDualProd_strictMono {α : Type u_1} [Preorder α] : StrictMono toDualProd

@[implicit_reducible]

instance NonemptyInterval.instCoeSet {α : Type u_1} [Preorder α] : Coe (NonemptyInterval α) (Set α)

@[implicit_reducible, instance 100]

instance NonemptyInterval.instMembership {α : Type u_1} [Preorder α] : Membership α (NonemptyInterval α)

@[simp]

theorem NonemptyInterval.mem_mk {α : Type u_1} [Preorder α] {x : α × α} {a : α} {hx : x.1 ≤ x.2} : a ∈ { toProd := x, fst_le_snd := hx } ↔ x.1 ≤ a ∧ a ≤ x.2

theorem NonemptyInterval.mem_def {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} : a ∈ s ↔ s.toProd.1 ≤ a ∧ a ≤ s.toProd.2

theorem NonemptyInterval.coe_nonempty {α : Type u_1} [Preorder α] (s : NonemptyInterval α) : (Set.Icc s.toProd.1 s.toProd.2).Nonempty

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

{a} as an interval.

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem NonemptyInterval.dual_pure {α : Type u_1} [Preorder α] (a : α) : dual (pure a) = pure (OrderDual.toDual a)

@[implicit_reducible]

instance NonemptyInterval.instInhabited {α : Type u_1} [Preorder α] [Inhabited α] : Inhabited (NonemptyInterval α)

instance NonemptyInterval.instNonempty {α : Type u_1} [Preorder α] [Nonempty α] : Nonempty (NonemptyInterval α)

instance NonemptyInterval.instNontrivial {α : Type u_1} [Preorder α] [Nontrivial α] : Nontrivial (NonemptyInterval α)

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

Pushforward of nonempty intervals.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

@[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✝¹ : NonemptyInterval β) : (map₂ f h₀ h₁ a✝ a✝¹).toProd.1 = f a✝.toProd.1 a✝¹.toProd.1

@[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✝¹ : NonemptyInterval β) : (map₂ f h₀ h₁ a✝ a✝¹).toProd.2 = f a✝.toProd.2 a✝¹.toProd.2

@[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 : β) : map₂ f h₀ h₁ (pure a) (pure b) = pure (f a b)

@[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 β) : dual (map₂ f h₀ h₁ s t) = map₂ (fun (a : αᵒᵈ) (b : βᵒᵈ) => OrderDual.toDual (f (OrderDual.ofDual a) (OrderDual.ofDual b))) ⋯ ⋯ (dual s) (dual t)

@[implicit_reducible]

instance NonemptyInterval.instOrderTop {α : Type u_1} [Preorder α] [BoundedOrder α] : OrderTop (NonemptyInterval α)

@[simp]

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

@[implicit_reducible]

instance NonemptyInterval.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (NonemptyInterval α)

@[implicit_reducible]

instance NonemptyInterval.instDecidableLE_1 {α : Type u_1} [PartialOrder α] [DecidableLE α] : DecidableLE (NonemptyInterval α)

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

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

@[implicit_reducible]

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

theorem NonemptyInterval.coe_subset_coe {α : Type u_1} [PartialOrder α] {s t : NonemptyInterval α} : ↑s ⊆ ↑t ↔ s ≤ t

theorem NonemptyInterval.coe_ssubset_coe {α : Type u_1} [PartialOrder α] {s t : NonemptyInterval α} : ↑s ⊂ ↑t ↔ s < t

@[simp]

theorem NonemptyInterval.coe_coeHom {α : Type u_1} [PartialOrder α] : ⇑coeHom = SetLike.coe

theorem NonemptyInterval.coe_def {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) : ↑s = Set.Icc s.toProd.1 s.toProd.2

@[simp]

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

@[simp]

theorem NonemptyInterval.mem_pure {α : Type u_1} [PartialOrder α] {a b : α} : b ∈ pure a ↔ b = a

@[simp]

theorem NonemptyInterval.coe_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] : ↑⊤ = Set.univ

@[simp]

theorem NonemptyInterval.coe_dual {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) : ↑(dual s) = ⇑OrderDual.ofDual ⁻¹' ↑s

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

@[implicit_reducible]

instance NonemptyInterval.instMax {α : Type u_1} [Lattice α] : Max (NonemptyInterval α)

@[implicit_reducible]

instance NonemptyInterval.instSemilatticeSup {α : Type u_1} [Lattice α] : SemilatticeSup (NonemptyInterval α)

@[simp]

theorem NonemptyInterval.fst_sup {α : Type u_1} [Lattice α] (s t : NonemptyInterval α) : (s ⊔ t).toProd.1 = s.toProd.1 ⊓ t.toProd.1

@[simp]

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

@[reducible, inline]

abbrev Interval (α : Type u_6) [LE α] : Type u_6

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

@[implicit_reducible]

instance Interval.instInhabited {α : Type u_1} [LE α] : Inhabited (Interval α)

@[implicit_reducible]

instance Interval.instLE {α : Type u_1} [LE α] : LE (Interval α)

@[implicit_reducible]

instance Interval.instOrderBot {α : Type u_1} [LE α] : OrderBot (Interval α)

@[implicit_reducible]

instance Interval.instCoeNonemptyInterval {α : Type u_1} [LE α] : Coe (NonemptyInterval α) (Interval α)

instance Interval.canLift {α : Type u_1} [LE α] : CanLift (Interval α) (NonemptyInterval α) WithBot.some fun (r : Interval α) => r ≠ ⊥

def Interval.recBotCoe {α : Type u_1} [LE α] {C : Interval α → Sort u_6} (bot : C ⊥) (coe : (a : NonemptyInterval α) → C ↑a) (n : Interval α) : C n

Recursor for Interval using the preferred forms ⊥ and ↑a.

theorem Interval.coe_injective {α : Type u_1} [LE α] : Function.Injective WithBot.some

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

theorem Interval.forall {α : Type u_1} [LE α] {p : Interval α → Prop} : (∀ (s : Interval α), p s) ↔ p ⊥ ∧ ∀ (s : NonemptyInterval α), p ↑s

theorem Interval.exists {α : Type u_1} [LE α] {p : Interval α → Prop} : (∃ (s : Interval α), p s) ↔ p ⊥ ∨ ∃ (s : NonemptyInterval α), p ↑s

@[implicit_reducible]

instance Interval.instUniqueOfIsEmpty {α : Type u_1} [LE α] [IsEmpty α] : Unique (Interval α)

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

Turn an interval into an interval in the dual order.

@[implicit_reducible]

instance Interval.instPreorder {α : Type u_1} [Preorder α] : Preorder (Interval α)

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

{a} as an interval.

theorem Interval.pure_injective {α : Type u_1} [Preorder α] : Function.Injective pure

@[simp]

theorem Interval.dual_pure {α : Type u_1} [Preorder α] (a : α) : dual (pure a) = pure (OrderDual.toDual a)

@[simp]

theorem Interval.dual_bot {α : Type u_1} [Preorder α] : dual ⊥ = ⊥

@[simp]

theorem Interval.pure_ne_bot {α : Type u_1} [Preorder α] {a : α} : pure a ≠ ⊥

@[simp]

theorem Interval.bot_ne_pure {α : Type u_1} [Preorder α] {a : α} : ⊥ ≠ pure a

instance Interval.instNontrivialOfNonempty {α : Type u_1} [Preorder α] [Nonempty α] : Nontrivial (Interval α)

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

Pushforward of intervals.

@[simp]

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

@[simp]

theorem Interval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) (s : Interval α) : map g (map f s) = map (g.comp f) s

@[simp]

theorem Interval.dual_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (s : Interval α) : dual (map f s) = map (OrderHom.dual f) (dual s)

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

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

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

@[implicit_reducible]

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

theorem Interval.coe_subset_coe {α : Type u_1} [PartialOrder α] {s t : Interval α} : ↑s ⊆ ↑t ↔ s ≤ t

theorem Interval.coe_sSubset_coe {α : Type u_1} [PartialOrder α] {s t : Interval α} : ↑s ⊂ ↑t ↔ s < t

@[simp]

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

@[simp]

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

@[simp]

theorem Interval.coe_bot {α : Type u_1} [PartialOrder α] : ↑⊥ = ∅

@[simp]

theorem Interval.coe_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] : ↑⊤ = Set.univ

@[simp]

theorem Interval.coe_dual {α : Type u_1} [PartialOrder α] (s : Interval α) : ↑(dual s) = ⇑OrderDual.ofDual ⁻¹' ↑s

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

@[simp]

theorem Interval.mem_pure {α : Type u_1} [PartialOrder α] {a b : α} : b ∈ pure a ↔ b = a

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Interval.lattice {α : Type u_1} [Lattice α] [DecidableLE α] : Lattice (Interval α)

@[simp]

theorem Interval.coe_inf {α : Type u_1} [Lattice α] [DecidableLE α] (s t : Interval α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

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

@[simp]

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

@[simp]

theorem NonemptyInterval.coe_eq_pure {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} : ↑s = Interval.pure a ↔ s = pure a

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

noncomputable instance Interval.completeLattice {α : Type u_1} [CompleteLattice α] [DecidableLE α] : CompleteLattice (Interval α)

@[simp]

theorem Interval.coe_sInf {α : Type u_1} [CompleteLattice α] [DecidableLE α] (S : Set (Interval α)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem Interval.coe_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [DecidableLE α] (f : ι → Interval α) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

theorem Interval.coe_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [CompleteLattice α] [DecidableLE α] (f : (i : ι) → κ i → Interval α) : ↑(⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), ↑(f i j)