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 : 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 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.toProd_injective {α : Type u_1} [LE α] : Function.Injective NonemptyInterval.toProd

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

theorem NonemptyInterval.ext_iff {α : Type u_1} [LE α] (s : NonemptyInterval α) (t : NonemptyInterval α) : s = t ↔ s.toProd = t.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 α) : NonemptyInterval.toDualProd s = (OrderDual.toDual s.toProd.1, s.toProd.2)

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

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

Equations

• (_ : IsEmpty (NonemptyInterval α)) = (_ : IsEmpty (NonemptyInterval α))

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

Equations

• (_ : Subsingleton (NonemptyInterval α)) = (_ : Subsingleton (NonemptyInterval α))

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

@[simp]

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

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

toDualProd as an order embedding.

Equations

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

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.instPreorderNonemptyIntervalToLE {α : Type u_1} [Preorder α] : Preorder (NonemptyInterval α)

Equations

• NonemptyInterval.instPreorderNonemptyIntervalToLE = Preorder.lift NonemptyInterval.toDualProd

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

Equations

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

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

Equations

• NonemptyInterval.instMembershipNonemptyIntervalToLE = { mem := fun (a : α) (s : NonemptyInterval α) => 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.Nonempty (Set.Icc s.toProd.1 s.toProd.2)

@[simp]

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

@[simp]

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

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

{a} as an interval.

Equations

• NonemptyInterval.pure a = { toProd := (a, a), fst_le_snd := (_ : (a, a).1 ≤ (a, a).1) }

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.instInhabitedNonemptyIntervalToLE {α : Type u_1} [Preorder α] [Inhabited α] : Inhabited (NonemptyInterval α)

Equations

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

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

Equations

• (_ : Nonempty (NonemptyInterval α)) = (_ : Nonempty (NonemptyInterval α))

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

Equations

• (_ : Nontrivial (NonemptyInterval α)) = (_ : Nontrivial (NonemptyInterval α))

@[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_snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) : (NonemptyInterval.map f a).toProd.2 = f a.1.2

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 := (_ : f a.1.1 ≤ f a.1.2) }

@[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 (OrderHom.comp g 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)

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

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

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

@[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))) (_ : ∀ (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)

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

Equations

• NonemptyInterval.instOrderTopNonemptyIntervalToLELe = OrderTop.mk (_ : ∀ (x : NonemptyInterval α), ⊤.toProd.1 ≤ x.toProd.1 ∧ x.toProd.2 ≤ ⊤.toProd.2)

@[simp]

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

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

Equations

• NonemptyInterval.instPartialOrderNonemptyIntervalToLEToPreorder = PartialOrder.lift NonemptyInterval.toDualProd (_ : Function.Injective NonemptyInterval.toDualProd)

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

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

Equations

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

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' := (_ : Function.Injective ⇑NonemptyInterval.coeHom) }

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

@[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.instSupNonemptyIntervalToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [Lattice α] : Sup (NonemptyInterval α)

Equations

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

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

Equations

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

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

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

Equations

• Interval α = WithBot (NonemptyInterval α)

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

Equations

• Interval.instInhabitedInterval = WithBot.inhabited

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

Equations

• Interval.instLEInterval = WithBot.le

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

Equations

• Interval.instOrderBotIntervalInstLEInterval = WithBot.orderBot

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

Equations

• Interval.instCoeNonemptyIntervalInterval = WithBot.coe

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

Equations

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

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.instUniqueInterval {α : Type u_1} [LE α] [IsEmpty α] : Unique (Interval α)

Equations

• Interval.instUniqueInterval = 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 = Equiv.optionCongr NonemptyInterval.dual

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

Equations

• Interval.instPreorderIntervalToLE = 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.instNontrivialIntervalToLE {α : Type u_1} [Preorder α] [Nonempty α] : Nontrivial (Interval α)

Equations

• (_ : Nontrivial (Interval α)) = (_ : Nontrivial (Option (NonemptyInterval α)))

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 (OrderHom.comp g 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

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

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

Equations

• Interval.setLike = { coe := ⇑Interval.coeHom, coe_injective' := (_ : Function.Injective ⇑Interval.coeHom) }

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 (x x_1 : α) => x ≤ x_1] : Lattice (Interval α)

Equations

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

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

@[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 (x x_1 : α) => x ≤ x_1] : CompleteLattice (Interval α)

Equations

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

@[simp]

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

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

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)