Documentation

Mathlib.Order.LatticeIntervals

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.

source
instance Set.Ico.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} {b : α} :
SemilatticeInf ↑(Set.Ico a b)
Equations
source
@[reducible]
def Set.Ico.orderBot {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a < b) :
OrderBot ↑(Set.Ico a b)

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

Equations
Instances For
    source
    instance Set.Iio.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
    SemilatticeInf ↑(Set.Iio a)
    Equations
    source
    instance Set.Ioc.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} {b : α} :
    SemilatticeSup ↑(Set.Ioc a b)
    Equations
    source
    @[reducible]
    def Set.Ioc.orderTop {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a < b) :
    OrderTop ↑(Set.Ioc a b)

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

    Equations
    Instances For
      source
      instance Set.Ioi.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
      SemilatticeSup ↑(Set.Ioi a)
      Equations
      source
      instance Set.Iic.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
      SemilatticeInf ↑(Set.Iic a)
      Equations
      source
      instance Set.Iic.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
      SemilatticeSup ↑(Set.Iic a)
      Equations
      source
      instance Set.Iic.instLatticeElemIicToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [Lattice α] {a : α} :
      Lattice ↑(Set.Iic a)
      Equations
      • Set.Iic.instLatticeElemIicToPreorderToPartialOrderToSemilatticeInf = let __src := Set.Iic.semilatticeInf; let __src_1 := Set.Iic.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯
      source
      instance Set.Iic.orderTop {α : Type u_1} [Preorder α] {a : α} :
      OrderTop ↑(Set.Iic a)
      Equations
      source
      @[simp]
      theorem Set.Iic.coe_top {α : Type u_1} [Preorder α] {a : α} :
      ↑⊤ = a
      source
      instance Set.Iic.orderBot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
      OrderBot ↑(Set.Iic a)
      Equations
      source
      @[simp]
      theorem Set.Iic.coe_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
      ↑⊥ = ⊥
      source
      instance Set.Iic.instBoundedOrderElemIicLeToLEMemSetInstMembershipSet {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
      BoundedOrder ↑(Set.Iic a)
      Equations
      • Set.Iic.instBoundedOrderElemIicLeToLEMemSetInstMembershipSet = let __src := Set.Iic.orderTop; let __src_1 := Set.Iic.orderBot; BoundedOrder.mk
      source
      instance Set.Ici.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
      SemilatticeInf ↑(Set.Ici a)
      Equations
      source
      instance Set.Ici.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
      SemilatticeSup ↑(Set.Ici a)
      Equations
      source
      instance Set.Ici.lattice {α : Type u_1} [Lattice α] {a : α} :
      Lattice ↑(Set.Ici a)
      Equations
      • Set.Ici.lattice = let __src := Set.Ici.semilatticeInf; let __src_1 := Set.Ici.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯
      source
      instance Set.Ici.distribLattice {α : Type u_1} [DistribLattice α] {a : α} :
      DistribLattice ↑(Set.Ici a)
      Equations
      source
      instance Set.Ici.orderBot {α : Type u_1} [Preorder α] {a : α} :
      OrderBot ↑(Set.Ici a)
      Equations
      source
      @[simp]
      theorem Set.Ici.coe_bot {α : Type u_1} [Preorder α] {a : α} :
      ↑⊥ = a
      source
      instance Set.Ici.orderTop {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
      OrderTop ↑(Set.Ici a)
      Equations
      source
      @[simp]
      theorem Set.Ici.coe_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
      ↑⊤ = ⊤
      source
      instance Set.Ici.boundedOrder {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
      BoundedOrder ↑(Set.Ici a)
      Equations
      • Set.Ici.boundedOrder = let __src := Set.Ici.orderTop; let __src_1 := Set.Ici.orderBot; BoundedOrder.mk
      source
      instance Set.Icc.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} {b : α} :
      SemilatticeInf ↑(Set.Icc a b)
      Equations
      source
      instance Set.Icc.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} {b : α} :
      SemilatticeSup ↑(Set.Icc a b)
      Equations
      source
      instance Set.Icc.lattice {α : Type u_1} [Lattice α] {a : α} {b : α} :
      Lattice ↑(Set.Icc a b)
      Equations
      • Set.Icc.lattice = let __src := Set.Icc.semilatticeInf; let __src_1 := Set.Icc.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯
      source
      @[reducible]
      def Set.Icc.orderBot {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ≤ b) :
      OrderBot ↑(Set.Icc a b)

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

      Equations
      Instances For
        source
        @[reducible]
        def Set.Icc.orderTop {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ≤ b) :
        OrderTop ↑(Set.Icc a b)

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

        Equations
        Instances For
          source
          @[reducible]
          def Set.Icc.boundedOrder {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ≤ b) :
          BoundedOrder ↑(Set.Icc a b)

          Icc a b is a BoundedOrder whenever a ≤ b.

          Equations
          Instances For