Documentation

Mathlib.Order.Interval.Basic

Order intervals #

This file defines (nonempty) closed intervals in an order (see Set.Icc). This is a prototype for interval arithmetic.

Main declarations #

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 {α : Type u_6} {inst✝ : LE α} {x y : NonemptyInterval α} (toProd : x.toProd = y.toProd) :
x = y
theorem NonemptyInterval.ext_iff {α : Type u_6} {inst✝ : LE α} {x y : NonemptyInterval α} :
x = y x.toProd = y.toProd
def NonemptyInterval.toDualProd {α : Type u_1} [LE α] :

The injection that induces the order on intervals.

Equations
instance NonemptyInterval.le {α : Type u_1} [LE α] :
Equations
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

toDualProd as an order embedding.

Equations
@[simp]

Turn an interval into an interval in the dual order.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
@[simp]
instance NonemptyInterval.instCoeSet {α : Type u_1} [Preorder α] :
Equations
@[instance 100]
Equations
@[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
def NonemptyInterval.pure {α : Type u_1} [Preorder α] (a : α) :

{a} as an interval.

Equations
@[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
@[simp]
theorem NonemptyInterval.dual_pure {α : Type u_1} [Preorder α] (a : α) :
def NonemptyInterval.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :

Pushforward of nonempty intervals.

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

Binary pushforward of nonempty intervals.

Equations
@[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)
Equations
@[simp]

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

Equations
Equations
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_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]
@[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)
Equations
@[simp]
theorem NonemptyInterval.fst_sup {α : Type u_1} [Lattice α] (s t : NonemptyInterval α) :
(st).toProd.1 = s.toProd.1t.toProd.1
@[simp]
theorem NonemptyInterval.snd_sup {α : Type u_1} [Lattice α] (s t : NonemptyInterval α) :
(st).toProd.2 = s.toProd.2t.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
instance Interval.instLE {α : Type u_1} [LE α] :
Equations
instance Interval.canLift {α : Type u_1} [LE α] :
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
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
def Interval.dual {α : Type u_1} [LE α] :

Turn an interval into an interval in the dual order.

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

{a} as an interval.

Equations
@[simp]
theorem Interval.dual_pure {α : Type u_1} [Preorder α] (a : α) :
@[simp]
theorem Interval.dual_bot {α : Type u_1} [Preorder α] :
@[simp]
theorem Interval.pure_ne_bot {α : Type u_1} [Preorder α] {a : α} :
@[simp]
theorem Interval.bot_ne_pure {α : Type u_1} [Preorder α] {a : α} :
def Interval.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
Interval αInterval β

Pushforward of intervals.

Equations
@[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)
@[simp]
theorem Interval.dual_top {α : Type u_1} [Preorder α] [BoundedOrder α] :
def Interval.coeHom {α : Type u_1} [PartialOrder α] :

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

Equations
instance Interval.setLike {α : Type u_1} [PartialOrder α] :
Equations
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 α] :
@[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
instance Interval.lattice {α : Type u_1} [Lattice α] [DecidableLE α] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Interval.coe_inf {α : Type u_1} [Lattice α] [DecidableLE α] (s t : Interval α) :
(st) = 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 : α) :
@[simp]
theorem NonemptyInterval.coe_eq_pure {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} :
s = Interval.pure a s = pure a
@[simp]
@[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 α) :
(st) = st
noncomputable instance Interval.completeLattice {α : Type u_1} [CompleteLattice α] [DecidableLE α] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Interval.coe_sInf {α : Type u_1} [CompleteLattice α] [DecidableLE α] (S : Set (Interval α)) :
(sInf S) = sS, 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 : ι) → κ iInterval α) :
(⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), (f i j)