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.

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

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

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

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

            Equations
              Instances For
                instance Set.Ioi.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
                Equations
                  instance Set.Iic.semilatticeInf {α : Type u_1} {a : α} [SemilatticeInf α] :
                  Equations
                    @[simp]
                    theorem Set.Iic.coe_inf {α : Type u_1} {a : α} [SemilatticeInf α] {x y : (Iic a)} :
                    (xy) = xy
                    instance Set.Iic.semilatticeSup {α : Type u_1} {a : α} [SemilatticeSup α] :
                    Equations
                      @[simp]
                      theorem Set.Iic.coe_sup {α : Type u_1} {a : α} [SemilatticeSup α] {x y : (Iic a)} :
                      (xy) = xy
                      instance Set.Iic.instLatticeElem {α : Type u_1} {a : α} [Lattice α] :
                      Lattice (Iic a)
                      Equations
                        instance Set.Iic.orderTop {α : Type u_1} {a : α} [Preorder α] :
                        OrderTop (Iic a)
                        Equations
                          @[simp]
                          theorem Set.Iic.coe_top {α : Type u_1} {a : α} [Preorder α] :
                          = a
                          theorem Set.Iic.eq_top_iff {α : Type u_1} {a : α} [Preorder α] {x : (Iic a)} :
                          x = x = a
                          instance Set.Iic.orderBot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] :
                          OrderBot (Iic a)
                          Equations
                            @[simp]
                            theorem Set.Iic.coe_bot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] :
                            =
                            instance Set.Iic.instBoundedOrderElemOfOrderBot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] :
                            Equations
                              theorem Set.Iic.disjoint_iff {α : Type u_1} {a : α} [SemilatticeInf α] [OrderBot α] {x y : (Iic a)} :
                              Disjoint x y Disjoint x y
                              theorem Set.Iic.codisjoint_iff {α : Type u_1} {a : α} [SemilatticeSup α] {x y : (Iic a)} :
                              Codisjoint x y xy = a
                              theorem Set.Iic.isCompl_iff {α : Type u_1} {a : α} [Lattice α] [OrderBot α] {x y : (Iic a)} :
                              IsCompl x y Disjoint x y xy = a
                              theorem Set.Iic.complementedLattice_iff {α : Type u_1} {a : α} [Lattice α] [OrderBot α] :
                              ComplementedLattice (Iic a) ba, ca, bc = bc = a
                              instance Set.Ici.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
                              Equations
                                instance Set.Ici.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
                                Equations
                                  instance Set.Ici.lattice {α : Type u_1} [Lattice α] {a : α} :
                                  Lattice (Ici a)
                                  Equations
                                    instance Set.Ici.distribLattice {α : Type u_1} [DistribLattice α] {a : α} :
                                    Equations
                                      instance Set.Ici.orderBot {α : Type u_1} [Preorder α] {a : α} :
                                      OrderBot (Ici a)
                                      Equations
                                        @[simp]
                                        theorem Set.Ici.coe_bot {α : Type u_1} [Preorder α] {a : α} :
                                        = a
                                        instance Set.Ici.orderTop {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
                                        OrderTop (Ici a)
                                        Equations
                                          @[simp]
                                          theorem Set.Ici.coe_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
                                          =
                                          instance Set.Ici.boundedOrder {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
                                          Equations
                                            instance Set.Icc.semilatticeInf {α : Type u_1} {a b : α} [SemilatticeInf α] :
                                            Equations
                                              instance Set.Icc.semilatticeSup {α : Type u_1} {a b : α} [SemilatticeSup α] :
                                              Equations
                                                instance Set.Icc.lattice {α : Type u_1} {a b : α} [Lattice α] :
                                                Lattice (Icc a b)
                                                Equations
                                                  instance Set.Icc.instOrderBotElem {α : Type u_1} {a b : α} [Preorder α] [Fact (a b)] :
                                                  OrderBot (Icc a b)

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

                                                  Equations
                                                    @[simp]
                                                    theorem Set.Icc.coe_bot {α : Type u_1} {a b : α} [Preorder α] [Fact (a b)] :
                                                    = a
                                                    instance Set.Icc.instOrderTopElem {α : Type u_1} {a b : α} [Preorder α] [Fact (a b)] :
                                                    OrderTop (Icc a b)

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

                                                    Equations
                                                      @[simp]
                                                      theorem Set.Icc.coe_top {α : Type u_1} {a b : α} [Preorder α] [Fact (a b)] :
                                                      = b
                                                      instance Set.Icc.instBoundedOrderElem {α : Type u_1} {a b : α} [Preorder α] [Fact (a b)] :
                                                      BoundedOrder (Icc a b)

                                                      Icc a b is a BoundedOrder whenever a ≤ b.

                                                      Equations