order.interval - mathlib3 docs

source

theorem nonempty_interval.ext {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) (h : x.to_prod = y.to_prod) :

x = y

source

@[ext]

structure nonempty_interval (α : Type u_7) [has_le α] :

Type u_7

to_prod : α × α
fst_le_snd : self.to_prod.fst ≤ self.to_prod.snd

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 nonempty_interval α → set α.

Instances for nonempty_interval

source

theorem nonempty_interval.ext_iff {α : Type u_7} {_inst_1 : has_le α} (x y : nonempty_interval α) :

x = y ↔ x.to_prod = y.to_prod

source

theorem nonempty_interval.to_prod_injective {α : Type u_1} [has_le α] :

function.injective nonempty_interval.to_prod

source

def nonempty_interval.to_dual_prod {α : Type u_1} [has_le α] :

nonempty_interval α → αᵒᵈ × α

The injection that induces the order on intervals.

Equations

nonempty_interval.to_dual_prod = nonempty_interval.to_prod

source

@[simp]

theorem nonempty_interval.to_dual_prod_apply {α : Type u_1} [has_le α] (s : nonempty_interval α) :

s.to_dual_prod = (⇑order_dual.to_dual s.to_prod.fst, s.to_prod.snd)

source

theorem nonempty_interval.to_dual_prod_injective {α : Type u_1} [has_le α] :

function.injective nonempty_interval.to_dual_prod

source

@[protected, instance]

def nonempty_interval.is_empty {α : Type u_1} [has_le α] [is_empty α] :

is_empty (nonempty_interval α)

source

@[protected, instance]

def nonempty_interval.subsingleton {α : Type u_1} [has_le α] [subsingleton α] :

subsingleton (nonempty_interval α)

source

@[protected, instance]

def nonempty_interval.has_le {α : Type u_1} [has_le α] :

has_le (nonempty_interval α)

Equations

nonempty_interval.has_le = {le := λ (s t : nonempty_interval α), t.to_prod.fst ≤ s.to_prod.fst ∧ s.to_prod.snd ≤ t.to_prod.snd}

source

theorem nonempty_interval.le_def {α : Type u_1} [has_le α] {s t : nonempty_interval α} :

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

source

def nonempty_interval.to_dual_prod_hom {α : Type u_1} [has_le α] :

nonempty_interval α ↪o αᵒᵈ × α

to_dual_prod as an order embedding.

Equations

nonempty_interval.to_dual_prod_hom = {to_embedding := {to_fun := nonempty_interval.to_dual_prod _inst_1, inj' := _}, map_rel_iff' := _}

source

@[simp]

theorem nonempty_interval.to_dual_prod_hom_apply {α : Type u_1} [has_le α] (ᾰ : nonempty_interval α) :

⇑nonempty_interval.to_dual_prod_hom ᾰ = ᾰ.to_dual_prod

source

def nonempty_interval.dual {α : Type u_1} [has_le α] :

nonempty_interval α ≃ nonempty_interval αᵒᵈ

Turn an interval into an interval in the dual order.

Equations

nonempty_interval.dual = {to_fun := λ (s : nonempty_interval α), {to_prod := s.to_prod.swap, fst_le_snd := _}, inv_fun := λ (s : nonempty_interval αᵒᵈ), {to_prod := s.to_prod.swap, fst_le_snd := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem nonempty_interval.fst_dual {α : Type u_1} [has_le α] (s : nonempty_interval α) :

(⇑nonempty_interval.dual s).to_prod.fst = ⇑order_dual.to_dual s.to_prod.snd

source

@[simp]

theorem nonempty_interval.snd_dual {α : Type u_1} [has_le α] (s : nonempty_interval α) :

(⇑nonempty_interval.dual s).to_prod.snd = ⇑order_dual.to_dual s.to_prod.fst

source

@[protected, instance]

def nonempty_interval.preorder {α : Type u_1} [preorder α] :

preorder (nonempty_interval α)

Equations

nonempty_interval.preorder = preorder.lift nonempty_interval.to_dual_prod

source

@[protected, instance]

def nonempty_interval.set.has_coe_t {α : Type u_1} [preorder α] :

has_coe_t (nonempty_interval α) (set α)

Equations

nonempty_interval.set.has_coe_t = {coe := λ (s : nonempty_interval α), set.Icc s.to_prod.fst s.to_prod.snd}

source

@[protected, instance]

def nonempty_interval.has_mem {α : Type u_1} [preorder α] :

has_mem α (nonempty_interval α)

Equations

nonempty_interval.has_mem = {mem := λ (a : α) (s : nonempty_interval α), a ∈ ↑s}

source

@[simp]

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

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

source

theorem nonempty_interval.mem_def {α : Type u_1} [preorder α] {s : nonempty_interval α} {a : α} :

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

source

@[simp]

theorem nonempty_interval.coe_nonempty {α : Type u_1} [preorder α] (s : nonempty_interval α) :

↑s.nonempty

source

@[simp]

theorem nonempty_interval.pure_to_prod {α : Type u_1} [preorder α] (a : α) :

(nonempty_interval.pure a).to_prod = (a, a)

source

def nonempty_interval.pure {α : Type u_1} [preorder α] (a : α) :

nonempty_interval α

{a} as an interval.

Equations

nonempty_interval.pure a = {to_prod := (a, a), fst_le_snd := _}

source

theorem nonempty_interval.mem_pure_self {α : Type u_1} [preorder α] (a : α) :

a ∈ nonempty_interval.pure a

source

theorem nonempty_interval.pure_injective {α : Type u_1} [preorder α] :

function.injective nonempty_interval.pure

source

@[simp]

theorem nonempty_interval.dual_pure {α : Type u_1} [preorder α] (a : α) :

⇑nonempty_interval.dual (nonempty_interval.pure a) = nonempty_interval.pure (⇑order_dual.to_dual a)

source

@[protected, instance]

def nonempty_interval.inhabited {α : Type u_1} [preorder α] [inhabited α] :

inhabited (nonempty_interval α)

Equations

nonempty_interval.inhabited = {default := nonempty_interval.pure inhabited.default}

source

@[protected, instance]

def nonempty_interval.nonempty {α : Type u_1} [preorder α] [nonempty α] :

nonempty (nonempty_interval α)

source

@[protected, instance]

def nonempty_interval.nontrivial {α : Type u_1} [preorder α] [nontrivial α] :

nontrivial (nonempty_interval α)

source

@[simp]

theorem nonempty_interval.map_to_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : nonempty_interval α) :

(nonempty_interval.map f a).to_prod = prod.map ⇑f ⇑f a.to_prod

source

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

nonempty_interval β

Pushforward of nonempty intervals.

Equations

nonempty_interval.map f a = {to_prod := prod.map ⇑f ⇑f a.to_prod, fst_le_snd := _}

source

@[simp]

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

nonempty_interval.map f (nonempty_interval.pure a) = nonempty_interval.pure (⇑f a)

source

@[simp]

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

nonempty_interval.map g (nonempty_interval.map f a) = nonempty_interval.map (g.comp f) a

source

@[simp]

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

⇑nonempty_interval.dual (nonempty_interval.map f a) = nonempty_interval.map (⇑order_hom.dual f) (⇑nonempty_interval.dual a)

source

@[simp]

theorem nonempty_interval.map₂_to_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), monotone (λ (a : α), f a b)) (h₁ : ∀ (a : α), monotone (f a)) (ᾰ : nonempty_interval α) (ᾰ_1 : nonempty_interval β) :

(nonempty_interval.map₂ f h₀ h₁ ᾰ ᾰ_1).to_prod = (f ᾰ.to_prod.fst ᾰ_1.to_prod.fst, f ᾰ.to_prod.snd ᾰ_1.to_prod.snd)

source

def nonempty_interval.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), monotone (λ (a : α), f a b)) (h₁ : ∀ (a : α), monotone (f a)) :

nonempty_interval α → nonempty_interval β → nonempty_interval γ

Binary pushforward of nonempty intervals.

Equations

nonempty_interval.map₂ f h₀ h₁ = λ (s : nonempty_interval α) (t : nonempty_interval β), {to_prod := (f s.to_prod.fst t.to_prod.fst, f s.to_prod.snd t.to_prod.snd), fst_le_snd := _}

source

@[simp]

theorem nonempty_interval.map₂_pure {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), monotone (λ (a : α), f a b)) (h₁ : ∀ (a : α), monotone (f a)) (a : α) (b : β) :

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

source

@[simp]

theorem nonempty_interval.dual_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α → β → γ) (h₀ : ∀ (b : β), monotone (λ (a : α), f a b)) (h₁ : ∀ (a : α), monotone (f a)) (s : nonempty_interval α) (t : nonempty_interval β) :

⇑nonempty_interval.dual (nonempty_interval.map₂ f h₀ h₁ s t) = nonempty_interval.map₂ (λ (a : αᵒᵈ) (b : βᵒᵈ), ⇑order_dual.to_dual (f (⇑order_dual.of_dual a) (⇑order_dual.of_dual b))) _ _ (⇑nonempty_interval.dual s) (⇑nonempty_interval.dual t)

source

@[protected, instance]

def nonempty_interval.order_top {α : Type u_1} [preorder α] [bounded_order α] :

order_top (nonempty_interval α)

Equations

nonempty_interval.order_top = {top := {to_prod := (⊥, ⊤), fst_le_snd := _}, le_top := _}

source

@[simp]

theorem nonempty_interval.dual_top {α : Type u_1} [preorder α] [bounded_order α] :

⇑nonempty_interval.dual ⊤ = ⊤

source

@[protected, instance]

def nonempty_interval.partial_order {α : Type u_1} [partial_order α] :

partial_order (nonempty_interval α)

Equations

nonempty_interval.partial_order = partial_order.lift nonempty_interval.to_dual_prod nonempty_interval.partial_order._proof_1

source

def nonempty_interval.coe_hom {α : Type u_1} [partial_order α] :

nonempty_interval α ↪o set α

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

Equations

nonempty_interval.coe_hom = order_embedding.of_map_le_iff (λ (s : nonempty_interval α), set.Icc s.to_prod.fst s.to_prod.snd) nonempty_interval.coe_hom._proof_1

source

@[protected, instance]

def nonempty_interval.set_like {α : Type u_1} [partial_order α] :

set_like (nonempty_interval α) α

Equations

nonempty_interval.set_like = {coe := λ (s : nonempty_interval α), set.Icc s.to_prod.fst s.to_prod.snd, coe_injective' := _}

source

@[simp, norm_cast]

theorem nonempty_interval.coe_subset_coe {α : Type u_1} [partial_order α] {s t : nonempty_interval α} :

↑s ⊆ ↑t ↔ s ≤ t

source

@[simp, norm_cast]

theorem nonempty_interval.coe_ssubset_coe {α : Type u_1} [partial_order α] {s t : nonempty_interval α} :

↑s ⊂ ↑t ↔ s < t

source

@[simp]

theorem nonempty_interval.coe_coe_hom {α : Type u_1} [partial_order α] :

⇑nonempty_interval.coe_hom = coe

source

@[simp, norm_cast]

theorem nonempty_interval.coe_pure {α : Type u_1} [partial_order α] (a : α) :

↑(nonempty_interval.pure a) = {a}

source

@[simp]

theorem nonempty_interval.mem_pure {α : Type u_1} [partial_order α] {a b : α} :

b ∈ nonempty_interval.pure a ↔ b = a

source

@[simp, norm_cast]

theorem nonempty_interval.coe_top {α : Type u_1} [partial_order α] [bounded_order α] :

↑⊤ = set.univ

source

@[simp, norm_cast]

theorem nonempty_interval.coe_dual {α : Type u_1} [partial_order α] (s : nonempty_interval α) :

↑(⇑nonempty_interval.dual s) = ⇑order_dual.of_dual ⁻¹' ↑s

source

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

⇑f '' ↑s ⊆ ↑(nonempty_interval.map f s)

source

@[protected, instance]

def nonempty_interval.has_sup {α : Type u_1} [lattice α] :

has_sup (nonempty_interval α)

Equations

nonempty_interval.has_sup = {sup := λ (s t : nonempty_interval α), {to_prod := (s.to_prod.fst ⊓ t.to_prod.fst, s.to_prod.snd ⊔ t.to_prod.snd), fst_le_snd := _}}

source

@[protected, instance]

def nonempty_interval.semilattice_sup {α : Type u_1} [lattice α] :

semilattice_sup (nonempty_interval α)

Equations

nonempty_interval.semilattice_sup = function.injective.semilattice_sup nonempty_interval.to_dual_prod nonempty_interval.semilattice_sup._proof_1 nonempty_interval.semilattice_sup._proof_2

source

@[simp]

theorem nonempty_interval.fst_sup {α : Type u_1} [lattice α] (s t : nonempty_interval α) :

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

source

@[simp]

theorem nonempty_interval.snd_sup {α : Type u_1} [lattice α] (s t : nonempty_interval α) :

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

source

@[protected, instance]

def interval.has_le (α : Type u_1) [has_le α] :

has_le (interval α)

source

def interval (α : Type u_1) [has_le α] :

Type u_1

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 α = with_bot (nonempty_interval α)

Instances for interval

source

@[protected, instance]

def interval.inhabited (α : Type u_1) [has_le α] :

inhabited (interval α)

source

@[protected, instance]

def interval.order_bot (α : Type u_1) [has_le α] :

order_bot (interval α)

source

@[protected, instance]

def interval.has_coe_t {α : Type u_1} [has_le α] :

has_coe_t (nonempty_interval α) (interval α)

Equations

interval.has_coe_t = with_bot.has_coe_t

source

@[protected, instance]

def interval.can_lift {α : Type u_1} [has_le α] :

can_lift (interval α) (nonempty_interval α) coe (λ (r : interval α), r ≠ ⊥)

Equations

interval.can_lift = with_bot.can_lift

source

theorem interval.coe_injective {α : Type u_1} [has_le α] :

function.injective coe

source

@[simp, norm_cast]

theorem interval.coe_inj {α : Type u_1} [has_le α] {s t : nonempty_interval α} :

↑s = ↑t ↔ s = t

source

@[protected]

theorem interval.forall {α : Type u_1} [has_le α] {p : interval α → Prop} :

(∀ (s : interval α), p s) ↔ p ⊥ ∧ ∀ (s : nonempty_interval α), p ↑s

source

@[protected]

theorem interval.exists {α : Type u_1} [has_le α] {p : interval α → Prop} :

(∃ (s : interval α), p s) ↔ p ⊥ ∨ ∃ (s : nonempty_interval α), p ↑s

source

@[protected, instance]

def interval.unique {α : Type u_1} [has_le α] [is_empty α] :

unique (interval α)

Equations

interval.unique = option.unique

source

def interval.dual {α : Type u_1} [has_le α] :

interval α ≃ interval αᵒᵈ

Turn an interval into an interval in the dual order.

Equations

interval.dual = nonempty_interval.dual.option_congr

source

@[protected, instance]

def interval.preorder {α : Type u_1} [preorder α] :

preorder (interval α)

Equations

interval.preorder = with_bot.preorder

source

def interval.pure {α : Type u_1} [preorder α] (a : α) :

interval α

{a} as an interval.

Equations

interval.pure a = ↑(nonempty_interval.pure a)

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 (⇑order_dual.to_dual 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

@[protected, instance]

def interval.nontrivial {α : 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.

Equations

interval.map f = with_bot.map (nonempty_interval.map f)

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 (g.comp 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 (⇑order_hom.dual f) (⇑interval.dual s)

source

@[protected, instance]

def interval.bounded_order {α : Type u_1} [preorder α] [bounded_order α] :

bounded_order (interval α)

Equations

interval.bounded_order = with_bot.bounded_order

source

@[simp]

theorem interval.dual_top {α : Type u_1} [preorder α] [bounded_order α] :

⇑interval.dual ⊤ = ⊤

source

@[protected, instance]

def interval.partial_order {α : Type u_1} [partial_order α] :

partial_order (interval α)

Equations

interval.partial_order = with_bot.partial_order

source

def interval.coe_hom {α : Type u_1} [partial_order α] :

interval α ↪o set α

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

Equations

interval.coe_hom = order_embedding.of_map_le_iff (λ (s : interval α), interval.coe_hom._match_1 s) interval.coe_hom._proof_1
interval.coe_hom._match_1 (option.some s) = ↑s
interval.coe_hom._match_1 ⊥ = ∅