Intervals in Lattices #
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*.semilattice_inf_botset.Ii*.semillatice_infset.I*c.semilattice_sup_topset.I*c.semillatice_infset.Iic.bounded_lattice, within abounded_latticeset.Ici.bounded_lattice, within abounded_lattice
@[instance]
def
set.Ico.semilattice_inf
{α : Type u_1}
{a b : α}
[semilattice_inf α] :
semilattice_inf ↥(set.Ico a b)
Equations
- set.Ico.semilattice_inf = subtype.semilattice_inf set.Ico.semilattice_inf._proof_1
Ico a b has a bottom element whenever a < b.
Equations
- set.Ico.order_bot h = {bot := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Ico a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Ico a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
def
set.Ico.semilattice_inf_bot
{α : Type u_1}
{a b : α}
[semilattice_inf α]
(h : a < b) :
semilattice_inf_bot ↥(set.Ico a b)
Ico a b is a semilattice_inf_bot whenever a < b.
Equations
- set.Ico.semilattice_inf_bot h = {bot := order_bot.bot (set.Ico.order_bot h), le := semilattice_inf.le set.Ico.semilattice_inf, lt := semilattice_inf.lt set.Ico.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf set.Ico.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
Equations
- set.Iio.semilattice_inf = subtype.semilattice_inf set.Iio.semilattice_inf._proof_1
@[instance]
def
set.Ioc.semilattice_sup
{α : Type u_1}
{a b : α}
[semilattice_sup α] :
semilattice_sup ↥(set.Ioc a b)
Equations
- set.Ioc.semilattice_sup = subtype.semilattice_sup set.Ioc.semilattice_sup._proof_1
Ioc a b has a top element whenever a < b.
Equations
- set.Ioc.order_top h = {top := ⟨b, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Ioc a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Ioc a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
def
set.Ioc.semilattice_sup_top
{α : Type u_1}
{a b : α}
[semilattice_sup α]
(h : a < b) :
semilattice_sup_top ↥(set.Ioc a b)
Ioc a b is a semilattice_sup_top whenever a < b.
Equations
- set.Ioc.semilattice_sup_top h = {top := order_top.top (set.Ioc.order_top h), le := semilattice_sup.le set.Ioc.semilattice_sup, lt := semilattice_sup.lt set.Ioc.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup set.Ioc.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
@[instance]
Equations
- set.Iio.set.Ioi.semilattice_sup = subtype.semilattice_sup set.Iio.set.Ioi.semilattice_sup._proof_1
@[instance]
Equations
- set.Iic.semilattice_inf = subtype.semilattice_inf set.Iic.semilattice_inf._proof_1
@[instance]
Equations
- set.Iic.semilattice_sup = subtype.semilattice_sup set.Iic.semilattice_sup._proof_1
@[instance]
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 := _}
@[instance]
Equations
- set.Iic.order_top = {top := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Iic a)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Iic a)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[instance]
Equations
- set.Iic.semilattice_inf_top = {top := order_top.top set.Iic.order_top, 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_top := _, inf := semilattice_inf.inf set.Iic.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
Equations
- set.Iic.semilattice_sup_top = {top := order_top.top set.Iic.order_top, le := semilattice_sup.le set.Iic.semilattice_sup, lt := semilattice_sup.lt set.Iic.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup set.Iic.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
@[instance]
Equations
- set.Iic.order_bot = {bot := ⟨⊥, _⟩, le := partial_order.le infer_instance, lt := partial_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[instance]
def
set.Iic.no_bot_order
{α : Type u_1}
[partial_order α]
[no_bot_order α]
{a : α} :
no_bot_order ↥(set.Iic a)
@[instance]
Equations
- set.Iic.semilattice_inf_bot = {bot := order_bot.bot set.Iic.order_bot, 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 := _, bot_le := _, inf := semilattice_inf.inf set.Iic.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
Equations
- set.Iic.semilattice_sup_bot = {bot := order_bot.bot set.Iic.order_bot, le := semilattice_sup.le set.Iic.semilattice_sup, lt := semilattice_sup.lt set.Iic.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup set.Iic.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
@[instance]
Equations
- set.Iic.bounded_lattice = {sup := lattice.sup set.Iic.lattice, le := order_top.le set.Iic.order_top, lt := order_top.lt set.Iic.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf set.Iic.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top set.Iic.order_top, le_top := _, bot := order_bot.bot set.Iic.order_bot, bot_le := _}
@[instance]
Equations
- set.Ici.semilattice_inf = subtype.semilattice_inf set.Ici.semilattice_inf._proof_1
@[instance]
Equations
- set.Ici.semilattice_sup = subtype.semilattice_sup set.Ici.semilattice_sup._proof_1
@[instance]
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 := _}
@[instance]
Equations
- set.Ici.order_bot = {bot := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Ici a)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Ici a)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[instance]
Equations
- set.Ici.semilattice_inf_bot = {bot := order_bot.bot set.Ici.order_bot, 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 := _, bot_le := _, inf := semilattice_inf.inf set.Ici.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
Equations
- set.Ici.semilattice_sup_bot = {bot := order_bot.bot set.Ici.order_bot, le := semilattice_sup.le set.Ici.semilattice_sup, lt := semilattice_sup.lt set.Ici.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup set.Ici.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
@[instance]
Equations
- set.Ici.order_top = {top := ⟨⊤, _⟩, le := partial_order.le infer_instance, lt := partial_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
@[instance]
def
set.Ici.no_top_order
{α : Type u_1}
[partial_order α]
[no_top_order α]
{a : α} :
no_top_order ↥(set.Ici a)
@[instance]
Equations
- set.Ici.semilattice_sup_top = {top := order_top.top set.Ici.order_top, le := semilattice_sup.le set.Ici.semilattice_sup, lt := semilattice_sup.lt set.Ici.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup set.Ici.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
@[instance]
Equations
- set.Ici.semilattice_inf_top = {top := order_top.top set.Ici.order_top, 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_top := _, inf := semilattice_inf.inf set.Ici.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
Equations
- set.Ici.bounded_lattice = {sup := lattice.sup set.Ici.lattice, le := order_top.le set.Ici.order_top, lt := order_top.lt set.Ici.order_top, 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 := _, top := order_top.top set.Ici.order_top, le_top := _, bot := order_bot.bot set.Ici.order_bot, bot_le := _}
@[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
@[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
@[instance]
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 := _}
Icc a b has a bottom element whenever a ≤ b.
Equations
- set.Icc.order_bot h = {bot := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
Icc a b has a top element whenever a ≤ b.
Equations
- set.Icc.order_top h = {top := ⟨b, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
def
set.Icc.semilattice_inf_bot
{α : Type u_1}
[semilattice_inf α]
{a b : α}
(h : a ≤ b) :
semilattice_inf_bot ↥(set.Icc a b)
Icc a b is a semilattice_inf_bot whenever a ≤ b.
Equations
- set.Icc.semilattice_inf_bot h = {bot := order_bot.bot (set.Icc.order_bot h), le := order_bot.le (set.Icc.order_bot h), lt := order_bot.lt (set.Icc.order_bot h), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf set.Icc.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
def
set.Icc.semilattice_inf_top
{α : Type u_1}
[semilattice_inf α]
{a b : α}
(h : a ≤ b) :
semilattice_inf_top ↥(set.Icc a b)
Icc a b is a semilattice_inf_top whenever a ≤ b.
Equations
- set.Icc.semilattice_inf_top h = {top := order_top.top (set.Icc.order_top h), le := order_top.le (set.Icc.order_top h), lt := order_top.lt (set.Icc.order_top h), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf set.Icc.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
def
set.Icc.semilattice_sup_bot
{α : Type u_1}
[semilattice_sup α]
{a b : α}
(h : a ≤ b) :
semilattice_sup_bot ↥(set.Icc a b)
Icc a b is a semilattice_sup_bot whenever a ≤ b.
Equations
- set.Icc.semilattice_sup_bot h = {bot := order_bot.bot (set.Icc.order_bot h), le := order_bot.le (set.Icc.order_bot h), lt := order_bot.lt (set.Icc.order_bot h), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup set.Icc.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
def
set.Icc.semilattice_sup_top
{α : Type u_1}
[semilattice_sup α]
{a b : α}
(h : a ≤ b) :
semilattice_sup_top ↥(set.Icc a b)
Icc a b is a semilattice_sup_top whenever a ≤ b.
Equations
- set.Icc.semilattice_sup_top h = {top := order_top.top (set.Icc.order_top h), le := order_top.le (set.Icc.order_top h), lt := order_top.lt (set.Icc.order_top h), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup set.Icc.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}
def
set.Icc.bounded_lattice
{α : Type u_1}
[lattice α]
{a b : α}
(h : a ≤ b) :
bounded_lattice ↥(set.Icc a b)
Icc a b is a bounded_lattice whenever a ≤ b.
Equations
- set.Icc.bounded_lattice h = {sup := semilattice_sup_top.sup (set.Icc.semilattice_sup_top h), le := semilattice_inf_bot.le (set.Icc.semilattice_inf_bot h), lt := semilattice_inf_bot.lt (set.Icc.semilattice_inf_bot h), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf_bot.inf (set.Icc.semilattice_inf_bot h), inf_le_left := _, inf_le_right := _, le_inf := _, top := semilattice_sup_top.top (set.Icc.semilattice_sup_top h), le_top := _, bot := semilattice_inf_bot.bot (set.Icc.semilattice_inf_bot h), bot_le := _}