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_bot
set.Ii*.semillatice_inf
set.I*c.semilattice_sup_top
set.I*c.semillatice_inf
set.Iic.bounded_lattice
, within abounded_lattice
set.Ici.bounded_lattice
, within abounded_lattice
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 := _}
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 := _}
Equations
- set.Iio.semilattice_inf = subtype.semilattice_inf set.Iio.semilattice_inf._proof_1
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 := _}
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 := _}
Equations
- set.Iio.set.Ioi.semilattice_sup = subtype.semilattice_sup set.Iio.set.Ioi.semilattice_sup._proof_1
Equations
- set.Iic.semilattice_inf = subtype.semilattice_inf set.Iic.semilattice_inf._proof_1
Equations
- set.Iic.semilattice_sup = subtype.semilattice_sup set.Iic.semilattice_sup._proof_1
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
Equations
- set.Ici.semilattice_inf = subtype.semilattice_inf set.Ici.semilattice_inf._proof_1
Equations
- set.Ici.semilattice_sup = subtype.semilattice_sup set.Ici.semilattice_sup._proof_1
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
Equations
- set.Icc.semilattice_inf = subtype.semilattice_inf set.Icc.semilattice_inf._proof_1
Equations
- set.Icc.semilattice_sup = subtype.semilattice_sup set.Icc.semilattice_sup._proof_1
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}
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 := _}