Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 19:29 f1d2bc60

View on Github →

feat(order/lattice_intervals): lattice structures on intervals in lattices (#5496) Defines (semi-)lattice structures on intervals in lattices

Estimated changes

Created src/order/lattice_intervals.lean

added def set.Icc.bounded_lattice

added def set.Icc.order_bot

added def set.Icc.order_top

added def set.Icc.semilattice_inf_bot

added def set.Icc.semilattice_inf_top

added def set.Icc.semilattice_sup_bot

added def set.Icc.semilattice_sup_top

added theorem set.Ici.coe_bot

added theorem set.Ici.coe_top

added def set.Ico.order_bot

added def set.Ico.semilattice_inf_bot

added theorem set.Iic.coe_bot

added theorem set.Iic.coe_top

added def set.Ioc.order_top

added def set.Ioc.semilattice_sup_top