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 Prod : 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 {α : Type u_6} : ∀ {inst : LE α} {x y : NonemptyInterval α}, x.toProd = y.toProd → x = y

theorem NonemptyInterval.fst_le_snd {α : Type u_6} [LE α] (self : NonemptyInterval α) : self.toProd.1 ≤ self.toProd.2

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

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

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

The injection that induces the order on intervals.

Equations

• NonemptyInterval.toDualProd = NonemptyInterval.toProd

@[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 NonemptyInterval.toDualProd

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• NonemptyInterval.le = { le := fun (s t : NonemptyInterval α) => t.toProd.1 ≤ s.toProd.1 ∧ s.toProd.2 ≤ t.toProd.2 }

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

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

toDualProd as an order embedding.

Equations

• NonemptyInterval.toDualProdHom = { toFun := NonemptyInterval.toDualProd, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

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

Turn an interval into an interval in the dual order.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• NonemptyInterval.instPreorder = Preorder.lift NonemptyInterval.toDualProd

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

Equations

• NonemptyInterval.instCoeSet = { coe := fun (s : NonemptyInterval α) => Set.Icc s.toProd.1 s.toProd.2 }

@[instance 100]

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

Equations

• NonemptyInterval.instMembership = { mem := fun (s : NonemptyInterval α) (a : α) => a ∈ Set.Icc s.toProd.1 s.toProd.2 }

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

Equations

• NonemptyInterval.pure a = { toProd := (a, a), fst_le_snd := ⋯ }

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

Equations

• NonemptyInterval.instInhabited = { default := NonemptyInterval.pure default }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Pushforward of nonempty intervals.

Equations

• NonemptyInterval.map f a = { toProd := Prod.map (⇑f) (⇑f) a.toProd, fst_le_snd := ⋯ }

@[simp]

theorem NonemptyInterval.map_snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) : (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 α) : (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 : α) : NonemptyInterval.map f (NonemptyInterval.pure a) = NonemptyInterval.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 α) : NonemptyInterval.map g (NonemptyInterval.map f a) = NonemptyInterval.map (g.comp f) a

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

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.

Equations

• NonemptyInterval.map₂ f h₀ h₁ s t = { toProd := (f s.toProd.1 t.toProd.1, f s.toProd.2 t.toProd.2), fst_le_snd := ⋯ }

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

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

Equations

• NonemptyInterval.instOrderTop = OrderTop.mk ⋯

@[simp]

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

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

Equations

• NonemptyInterval.instPartialOrder = PartialOrder.lift NonemptyInterval.toDualProd ⋯

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

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

Equations

• NonemptyInterval.coeHom = OrderEmbedding.ofMapLEIff (fun (s : NonemptyInterval α) => Set.Icc s.toProd.1 s.toProd.2) ⋯

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

Equations

• NonemptyInterval.setLike = { coe := fun (s : NonemptyInterval α) => Set.Icc s.toProd.1 s.toProd.2, coe_injective' := ⋯ }

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

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

@[simp]

theorem NonemptyInterval.coe_coeHom {α : Type u_1} [PartialOrder α] : ⇑NonemptyInterval.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 : α) : ↑(NonemptyInterval.pure a) = {a}

@[simp]

theorem NonemptyInterval.mem_pure {α : Type u_1} [PartialOrder α] {a : α} {b : α} : b ∈ NonemptyInterval.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 α) : ↑(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 ⊆ ↑(NonemptyInterval.map f s)

instance NonemptyInterval.instSup {α : Type u_1} [Lattice α] : Sup (NonemptyInterval α)

Equations

• NonemptyInterval.instSup = { sup := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 ⊓ t.toProd.1, s.toProd.2 ⊔ t.toProd.2), fst_le_snd := ⋯ } }

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

Equations

• NonemptyInterval.instSemilatticeSup = Function.Injective.semilatticeSup NonemptyInterval.toDualProd ⋯ ⋯

@[simp]

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

@[simp]

theorem NonemptyInterval.snd_sup {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (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 α.

Equations

• Interval α = WithBot (NonemptyInterval α)

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

Equations

• Interval.instInhabited = WithBot.inhabited

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

Equations

• Interval.instLE = WithBot.le

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

Equations

• Interval.instOrderBot = WithBot.orderBot

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

Equations

• Interval.instCoeNonemptyInterval = WithBot.coe

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

Equations

• ⋯ = ⋯

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.

Equations

• Interval.recBotCoe bot coe n = WithBot.recBotCoe bot coe n

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

theorem Interval.coe_inj {α : Type u_1} [LE α] {s : NonemptyInterval α} {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

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

Equations

• Interval.instUniqueOfIsEmpty = inferInstanceAs (Unique (Option (NonemptyInterval α)))

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

Turn an interval into an interval in the dual order.

Equations

• Interval.dual = NonemptyInterval.dual.optionCongr

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

Equations

• Interval.instPreorder = WithBot.preorder

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

{a} as an interval.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Pushforward of intervals.

Equations

• Interval.map f = WithBot.map (NonemptyInterval.map f)

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

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

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

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

Equations

• Interval.boundedOrder = WithBot.instBoundedOrder

@[simp]

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

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

Equations

• Interval.partialOrder = WithBot.partialOrder

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

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

Equations

• Interval.coeHom = OrderEmbedding.ofMapLEIff (fun (s : Interval α) => match s with | none => ∅ | some s => ↑s) ⋯

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

Equations

• Interval.setLike = { coe := ⇑Interval.coeHom, coe_injective' := ⋯ }

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

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

@[simp]

theorem Interval.coe_pure {α : Type u_1} [PartialOrder α] (a : α) : ↑(Interval.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 α) : ↑(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 ⊆ ↑(Interval.map f s)

@[simp]

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

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

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

Equations

• Interval.semilatticeSup = WithBot.semilatticeSup

instance Interval.lattice {α : Type u_1} [Lattice α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Lattice (Interval α)

Equations

• Interval.lattice = Lattice.mk ⋯ ⋯ ⋯

@[simp]

theorem Interval.coe_inf {α : Type u_1} [Lattice α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (s : Interval α) (t : Interval α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

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

@[simp]

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

@[simp]

theorem NonemptyInterval.coe_eq_pure {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} : ↑s = Interval.pure a ↔ s = NonemptyInterval.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 : NonemptyInterval α) (t : NonemptyInterval α) : ↑(s ⊔ t) = ↑s ⊔ ↑t

noncomputable instance Interval.completeLattice {α : Type u_1} [CompleteLattice α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : CompleteLattice (Interval α)

Equations

• Interval.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Interval.coe_sInf {α : Type u_1} [CompleteLattice α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (S : Set (Interval α)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem Interval.coe_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (f : ι → Interval α) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

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