mathlib3 documentation

order.lattice_intervals

Intervals in Lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we provide instances of lattice structures on intervals within lattices. Some of them depend on the order of the endpoints of the interval, and thus are not made global instances. These are probably not all of the lattice instances that could be placed on these intervals, but more can be added easily along the same lines when needed.

Main definitions #

In the following, * can represent either c, o, or i.

set.Ic*.order_bot
set.Ii*.semillatice_inf
set.I*c.order_top
set.I*c.semillatice_inf
set.I**.lattice
set.Iic.bounded_order, within an order_bot
set.Ici.bounded_order, within an order_top

@[protected, instance]

def set.Ico.semilattice_inf {α : Type u_1} [semilattice_inf α] {a b : α} :

semilattice_inf ↥(set.Ico a b)

Equations

set.Ico.semilattice_inf = subtype.semilattice_inf set.Ico.semilattice_inf._proof_1

@[protected, reducible]

def set.Ico.order_bot {α : Type u_1} [partial_order α] {a b : α} (h : a < b) :

order_bot ↥(set.Ico a b)

Ico a b has a bottom element whenever a < b.

Equations

set.Ico.order_bot h = _.order_bot

@[protected, instance]

def set.Iio.semilattice_inf {α : Type u_1} [semilattice_inf α] {a : α} :

semilattice_inf ↥(set.Iio a)

Equations

set.Iio.semilattice_inf = subtype.semilattice_inf set.Iio.semilattice_inf._proof_1

@[protected, instance]

def set.Ioc.semilattice_sup {α : Type u_1} [semilattice_sup α] {a b : α} :

semilattice_sup ↥(set.Ioc a b)

Equations

set.Ioc.semilattice_sup = subtype.semilattice_sup set.Ioc.semilattice_sup._proof_1

@[protected, reducible]

def set.Ioc.order_top {α : Type u_1} [partial_order α] {a b : α} (h : a < b) :

order_top ↥(set.Ioc a b)

Ioc a b has a top element whenever a < b.

Equations

set.Ioc.order_top h = _.order_top

@[protected, instance]

def set.Ioi.semilattice_sup {α : Type u_1} [semilattice_sup α] {a : α} :

semilattice_sup ↥(set.Ioi a)

Equations

set.Ioi.semilattice_sup = subtype.semilattice_sup set.Ioi.semilattice_sup._proof_1

@[protected, instance]

def set.Iic.semilattice_inf {α : Type u_1} [semilattice_inf α] {a : α} :

semilattice_inf ↥(set.Iic a)

Equations

set.Iic.semilattice_inf = subtype.semilattice_inf set.Iic.semilattice_inf._proof_1

@[protected, instance]

def set.Iic.semilattice_sup {α : Type u_1} [semilattice_sup α] {a : α} :

semilattice_sup ↥(set.Iic a)

Equations

set.Iic.semilattice_sup = subtype.semilattice_sup set.Iic.semilattice_sup._proof_1

@[protected, instance]

def set.Iic.lattice {α : Type u_1} [lattice α] {a : α} :

lattice ↥(set.Iic a)

Equations

set.Iic.lattice = {sup := semilattice_sup.sup set.Iic.semilattice_sup, le := semilattice_inf.le set.Iic.semilattice_inf, lt := semilattice_inf.lt set.Iic.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf set.Iic.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[protected, instance]

def set.Iic.order_top {α : Type u_1} [preorder α] {a : α} :

order_top ↥(set.Iic a)

Equations

set.Iic.order_top = {top := ⟨a, _⟩, le_top := _}

@[simp]

theorem set.Iic.coe_top {α : Type u_1} [preorder α] {a : α} :

@[protected, instance]

def set.Iic.order_bot {α : Type u_1} [preorder α] [order_bot α] {a : α} :

order_bot ↥(set.Iic a)

Equations

set.Iic.order_bot = {bot := ⟨⊥, _⟩, bot_le := _}

@[simp]

theorem set.Iic.coe_bot {α : Type u_1} [preorder α] [order_bot α] {a : α} :

@[protected, instance]

def set.Iic.bounded_order {α : Type u_1} [preorder α] [order_bot α] {a : α} :

bounded_order ↥(set.Iic a)

Equations

set.Iic.bounded_order = {top := order_top.top set.Iic.order_top, le_top := _, bot := order_bot.bot set.Iic.order_bot, bot_le := _}

@[protected, instance]

def set.Ici.semilattice_inf {α : Type u_1} [semilattice_inf α] {a : α} :

semilattice_inf ↥(set.Ici a)

Equations

set.Ici.semilattice_inf = subtype.semilattice_inf set.Ici.semilattice_inf._proof_1

@[protected, instance]

def set.Ici.semilattice_sup {α : Type u_1} [semilattice_sup α] {a : α} :

semilattice_sup ↥(set.Ici a)

Equations

set.Ici.semilattice_sup = subtype.semilattice_sup set.Ici.semilattice_sup._proof_1

@[protected, instance]

def set.Ici.lattice {α : Type u_1} [lattice α] {a : α} :

lattice ↥(set.Ici a)

Equations

set.Ici.lattice = {sup := semilattice_sup.sup set.Ici.semilattice_sup, le := semilattice_inf.le set.Ici.semilattice_inf, lt := semilattice_inf.lt set.Ici.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf set.Ici.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[protected, instance]

def set.Ici.distrib_lattice {α : Type u_1} [distrib_lattice α] {a : α} :

distrib_lattice ↥(set.Ici a)

Equations

set.Ici.distrib_lattice = {sup := lattice.sup set.Ici.lattice, le := lattice.le set.Ici.lattice, lt := lattice.lt set.Ici.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf set.Ici.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

@[protected, instance]

def set.Ici.order_bot {α : Type u_1} [preorder α] {a : α} :

order_bot ↥(set.Ici a)

Equations

set.Ici.order_bot = {bot := ⟨a, _⟩, bot_le := _}

@[simp]

theorem set.Ici.coe_bot {α : Type u_1} [preorder α] {a : α} :

@[protected, instance]

def set.Ici.order_top {α : Type u_1} [preorder α] [order_top α] {a : α} :

order_top ↥(set.Ici a)

Equations

set.Ici.order_top = {top := ⟨⊤, _⟩, le_top := _}

@[simp]

theorem set.Ici.coe_top {α : Type u_1} [preorder α] [order_top α] {a : α} :

@[protected, instance]

def set.Ici.bounded_order {α : Type u_1} [preorder α] [order_top α] {a : α} :

bounded_order ↥(set.Ici a)

Equations

set.Ici.bounded_order = {top := order_top.top set.Ici.order_top, le_top := _, bot := order_bot.bot set.Ici.order_bot, bot_le := _}

@[protected, instance]

def set.Icc.semilattice_inf {α : Type u_1} [semilattice_inf α] {a b : α} :

semilattice_inf ↥(set.Icc a b)

Equations

set.Icc.semilattice_inf = subtype.semilattice_inf set.Icc.semilattice_inf._proof_1

@[protected, instance]

def set.Icc.semilattice_sup {α : Type u_1} [semilattice_sup α] {a b : α} :

semilattice_sup ↥(set.Icc a b)

Equations

set.Icc.semilattice_sup = subtype.semilattice_sup set.Icc.semilattice_sup._proof_1

@[protected, instance]

def set.Icc.lattice {α : Type u_1} [lattice α] {a b : α} :

lattice ↥(set.Icc a b)

Equations

set.Icc.lattice = {sup := semilattice_sup.sup set.Icc.semilattice_sup, le := semilattice_inf.le set.Icc.semilattice_inf, lt := semilattice_inf.lt set.Icc.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf set.Icc.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[protected, reducible]

def set.Icc.order_bot {α : Type u_1} [preorder α] {a b : α} (h : a ≤ b) :

order_bot ↥(set.Icc a b)

Icc a b has a bottom element whenever a ≤ b.

Equations

set.Icc.order_bot h = _.order_bot

@[protected, reducible]

def set.Icc.order_top {α : Type u_1} [preorder α] {a b : α} (h : a ≤ b) :

order_top ↥(set.Icc a b)

Icc a b has a top element whenever a ≤ b.

Equations

set.Icc.order_top h = _.order_top

@[protected, reducible]

def set.Icc.bounded_order {α : Type u_1} [preorder α] {a b : α} (h : a ≤ b) :

bounded_order ↥(set.Icc a b)

Icc a b is a bounded_order whenever a ≤ b.

Equations

set.Icc.bounded_order h = {top := order_top.top (set.Icc.order_top h), le_top := _, bot := order_bot.bot (set.Icc.order_bot h), bot_le := _}