Documentation

Mathlib.Order.BoundedOrder.Basic

⊤ and ⊥, bounded lattices and variants #

This file defines top and bottom elements (greatest and least elements) of a type, the bounded variants of different kinds of lattices, sets up the typeclass hierarchy between them and provides instances for Prop and fun.

Main declarations #

Top, bottom element #

class OrderTop (α : Type u) [LE α] extends Top α :

An order is an OrderTop if it has a greatest element. We state this using a data mixin, holding the value of and the greatest element constraint.

  • top : α
  • le_top (a : α) : a

    is the greatest element

Instances
    noncomputable def topOrderOrNoTopOrder (α : Type u_1) [LE α] :

    An order is (noncomputably) either an OrderTop or a NoTopOrder. Use as casesI topOrderOrNoTopOrder α.

    Equations
      Instances For
        @[simp]
        theorem le_top {α : Type u} [LE α] [OrderTop α] {a : α} :
        @[simp]
        theorem isTop_top {α : Type u} [LE α] [OrderTop α] :
        def IsTop.rec {α : Type u} [LE α] {P : (x : α) → IsTop xSort u_1} (h : [inst : OrderTop α] → P ) (x : α) (hx : IsTop x) :
        P x hx

        A top element can be replaced with .

        Prefer IsTop.eq_top if α already has a top element.

        Equations
          Instances For
            @[simp]
            theorem isMax_top {α : Type u} [Preorder α] [OrderTop α] :
            @[simp]
            theorem not_top_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} :
            theorem ne_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) :
            theorem LT.lt.ne_top {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) :

            Alias of ne_top_of_lt.

            theorem lt_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) :
            a <
            theorem LT.lt.lt_top {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) :
            a <

            Alias of lt_top_of_lt.

            @[simp]
            theorem isMax_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            @[simp]
            theorem isTop_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            theorem not_isMax_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            theorem not_isTop_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            theorem IsMax.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            IsMax aa =

            Alias of the forward direction of isMax_iff_eq_top.

            theorem IsTop.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            IsTop aa =

            Alias of the forward direction of isTop_iff_eq_top.

            @[simp]
            theorem top_le_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            theorem top_unique {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a) :
            a =
            theorem eq_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            theorem eq_top_mono {α : Type u} [PartialOrder α] [OrderTop α] {a b : α} (h : a b) (h₂ : a = ) :
            b =
            theorem lt_top_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            @[simp]
            theorem not_lt_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
            theorem eq_top_or_lt_top {α : Type u} [PartialOrder α] [OrderTop α] (a : α) :
            a = a <
            theorem Ne.lt_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a ) :
            a <
            theorem Ne.lt_top' {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a) :
            a <
            theorem ne_top_of_le_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a b : α} (hb : b ) (hab : a b) :
            theorem top_notMem_iff {α : Type u} [PartialOrder α] [OrderTop α] {s : Set α} :
            ¬ s ∀ (x : α), x sx <
            @[deprecated top_notMem_iff (since := "2025-05-23")]
            theorem top_not_mem_iff {α : Type u} [PartialOrder α] [OrderTop α] {s : Set α} :
            ¬ s ∀ (x : α), x sx <

            Alias of top_notMem_iff.

            theorem OrderTop.ext_top {α : Type u_1} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x y x y) :
            class OrderBot (α : Type u) [LE α] extends Bot α :

            An order is an OrderBot if it has a least element. We state this using a data mixin, holding the value of and the least element constraint.

            • bot : α
            • bot_le (a : α) : a

              is the least element

            Instances
              noncomputable def botOrderOrNoBotOrder (α : Type u_1) [LE α] :

              An order is (noncomputably) either an OrderBot or a NoBotOrder. Use as casesI botOrderOrNoBotOrder α.

              Equations
                Instances For
                  @[simp]
                  theorem bot_le {α : Type u} [LE α] [OrderBot α] {a : α} :
                  @[simp]
                  theorem isBot_bot {α : Type u} [LE α] [OrderBot α] :
                  def IsBot.rec {α : Type u} [LE α] {P : (x : α) → IsBot xSort u_1} (h : [inst : OrderBot α] → P ) (x : α) (hx : IsBot x) :
                  P x hx

                  A bottom element can be replaced with .

                  Prefer IsBot.eq_bot if α already has a bottom element.

                  Equations
                    Instances For
                      instance OrderDual.instTop (α : Type u) [Bot α] :
                      Equations
                        instance OrderDual.instBot (α : Type u) [Top α] :
                        Equations
                          instance OrderDual.instOrderTop (α : Type u) [LE α] [OrderBot α] :
                          Equations
                            instance OrderDual.instOrderBot (α : Type u) [LE α] [OrderTop α] :
                            Equations
                              @[simp]
                              theorem OrderDual.ofDual_bot (α : Type u) [Top α] :
                              @[simp]
                              theorem OrderDual.ofDual_top (α : Type u) [Bot α] :
                              @[simp]
                              theorem OrderDual.toDual_bot (α : Type u) [Bot α] :
                              @[simp]
                              theorem OrderDual.toDual_top (α : Type u) [Top α] :
                              @[simp]
                              theorem isMin_bot {α : Type u} [Preorder α] [OrderBot α] :
                              @[simp]
                              theorem not_lt_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} :
                              theorem ne_bot_of_gt {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : a < b) :
                              theorem LT.lt.ne_bot {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : a < b) :

                              Alias of ne_bot_of_gt.

                              theorem bot_lt_of_lt {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : a < b) :
                              < b
                              theorem LT.lt.bot_lt {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : a < b) :
                              < b

                              Alias of bot_lt_of_lt.

                              @[simp]
                              theorem isMin_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              @[simp]
                              theorem isBot_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              theorem not_isMin_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              theorem not_isBot_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              theorem IsMin.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              IsMin aa =

                              Alias of the forward direction of isMin_iff_eq_bot.

                              theorem IsBot.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              IsBot aa =

                              Alias of the forward direction of isBot_iff_eq_bot.

                              @[simp]
                              theorem le_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              theorem bot_unique {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ) :
                              a =
                              theorem eq_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              theorem eq_bot_mono {α : Type u} [PartialOrder α] [OrderBot α] {a b : α} (h : a b) (h₂ : b = ) :
                              a =
                              theorem bot_lt_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              @[simp]
                              theorem not_bot_lt_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
                              theorem eq_bot_or_bot_lt {α : Type u} [PartialOrder α] [OrderBot α] (a : α) :
                              a = < a
                              theorem eq_bot_of_minimal {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ∀ (b : α), ¬b < a) :
                              a =
                              theorem Ne.bot_lt {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ) :
                              < a
                              theorem Ne.bot_lt' {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a) :
                              < a
                              theorem ne_bot_of_le_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a b : α} (hb : b ) (hab : b a) :
                              theorem bot_notMem_iff {α : Type u} [PartialOrder α] [OrderBot α] {s : Set α} :
                              ¬ s ∀ (x : α), x s < x
                              @[deprecated bot_notMem_iff (since := "2025-05-23")]
                              theorem bot_not_mem_iff {α : Type u} [PartialOrder α] [OrderBot α] {s : Set α} :
                              ¬ s ∀ (x : α), x s < x

                              Alias of bot_notMem_iff.

                              theorem OrderBot.ext_bot {α : Type u_1} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α) (H : ∀ (x y : α), x y x y) :

                              Bounded order #

                              class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α :

                              A bounded order describes an order (≤) with a top and bottom element, denoted and respectively.

                              Instances

                                Function lattices #

                                instance Pi.instBotForall {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Bot (α' i)] :
                                Bot ((i : ι) → α' i)
                                Equations
                                  @[simp]
                                  theorem Pi.bot_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Bot (α' i)] (i : ι) :
                                  theorem Pi.bot_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Bot (α' i)] :
                                  = fun (x : ι) =>
                                  @[simp]
                                  theorem Pi.bot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Bot γ] (x : αβ) :
                                  instance Pi.instTopForall {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Top (α' i)] :
                                  Top ((i : ι) → α' i)
                                  Equations
                                    @[simp]
                                    theorem Pi.top_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Top (α' i)] (i : ι) :
                                    theorem Pi.top_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Top (α' i)] :
                                    = fun (x : ι) =>
                                    @[simp]
                                    theorem Pi.top_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Top γ] (x : αβ) :
                                    instance Pi.instOrderTop {ι : Type u_1} {α' : ιType u_2} [(i : ι) → LE (α' i)] [(i : ι) → OrderTop (α' i)] :
                                    OrderTop ((i : ι) → α' i)
                                    Equations
                                      instance Pi.instOrderBot {ι : Type u_1} {α' : ιType u_2} [(i : ι) → LE (α' i)] [(i : ι) → OrderBot (α' i)] :
                                      OrderBot ((i : ι) → α' i)
                                      Equations
                                        instance Pi.instBoundedOrder {ι : Type u_1} {α' : ιType u_2} [(i : ι) → LE (α' i)] [(i : ι) → BoundedOrder (α' i)] :
                                        BoundedOrder ((i : ι) → α' i)
                                        Equations
                                          theorem eq_bot_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] ( : = ) (x : α) :
                                          x =
                                          theorem eq_top_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] ( : = ) (x : α) :
                                          x =
                                          @[reducible, inline]
                                          abbrev OrderTop.lift {α : Type u} {β : Type v} [LE α] [Top α] [LE β] [OrderTop β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) :

                                          Pullback an OrderTop.

                                          Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev OrderBot.lift {α : Type u} {β : Type v} [LE α] [Bot α] [LE β] [OrderBot β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_bot : f = ) :

                                              Pullback an OrderBot.

                                              Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev BoundedOrder.lift {α : Type u} {β : Type v} [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) (map_bot : f = ) :

                                                  Pullback a BoundedOrder.

                                                  Equations
                                                    Instances For

                                                      Subtype, order dual, product lattices #

                                                      @[reducible, inline]
                                                      abbrev Subtype.orderBot {α : Type u} {p : αProp} [LE α] [OrderBot α] (hbot : p ) :
                                                      OrderBot { x : α // p x }

                                                      A subtype remains a -order if the property holds at .

                                                      Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev Subtype.orderTop {α : Type u} {p : αProp} [LE α] [OrderTop α] (htop : p ) :
                                                          OrderTop { x : α // p x }

                                                          A subtype remains a -order if the property holds at .

                                                          Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev Subtype.boundedOrder {α : Type u} {p : αProp} [LE α] [BoundedOrder α] (hbot : p ) (htop : p ) :

                                                              A subtype remains a bounded order if the property holds at and .

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Subtype.mk_bot {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) :
                                                                  @[simp]
                                                                  theorem Subtype.mk_top {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) :
                                                                  theorem Subtype.coe_bot {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) :
                                                                  =
                                                                  theorem Subtype.coe_top {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) :
                                                                  =
                                                                  @[simp]
                                                                  theorem Subtype.coe_eq_bot_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) {x : { x : α // p x }} :
                                                                  x = x =
                                                                  @[simp]
                                                                  theorem Subtype.coe_eq_top_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) {x : { x : α // p x }} :
                                                                  x = x =
                                                                  @[simp]
                                                                  theorem Subtype.mk_eq_bot_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) {x : α} (hx : p x) :
                                                                  x, hx = x =
                                                                  @[simp]
                                                                  theorem Subtype.mk_eq_top_iff {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) {x : α} (hx : p x) :
                                                                  x, hx = x =
                                                                  instance Prod.instTop (α : Type u) (β : Type v) [Top α] [Top β] :
                                                                  Top (α × β)
                                                                  Equations
                                                                    instance Prod.instBot (α : Type u) (β : Type v) [Bot α] [Bot β] :
                                                                    Bot (α × β)
                                                                    Equations
                                                                      @[simp]
                                                                      theorem Prod.fst_top (α : Type u) (β : Type v) [Top α] [Top β] :
                                                                      @[simp]
                                                                      theorem Prod.snd_top (α : Type u) (β : Type v) [Top α] [Top β] :
                                                                      @[simp]
                                                                      theorem Prod.fst_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
                                                                      @[simp]
                                                                      theorem Prod.snd_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
                                                                      instance Prod.instOrderTop (α : Type u) (β : Type v) [LE α] [LE β] [OrderTop α] [OrderTop β] :
                                                                      OrderTop (α × β)
                                                                      Equations
                                                                        instance Prod.instOrderBot (α : Type u) (β : Type v) [LE α] [LE β] [OrderBot α] [OrderBot β] :
                                                                        OrderBot (α × β)
                                                                        Equations
                                                                          instance Prod.instBoundedOrder (α : Type u) (β : Type v) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] :
                                                                          Equations
                                                                            instance ULift.instTop {α : Type u} [Top α] :
                                                                            Equations
                                                                              @[simp]
                                                                              theorem ULift.up_top {α : Type u} [Top α] :
                                                                              { down := } =
                                                                              @[simp]
                                                                              theorem ULift.down_top {α : Type u} [Top α] :
                                                                              instance ULift.instBot {α : Type u} [Bot α] :
                                                                              Equations
                                                                                @[simp]
                                                                                theorem ULift.up_bot {α : Type u} [Bot α] :
                                                                                { down := } =
                                                                                @[simp]
                                                                                theorem ULift.down_bot {α : Type u} [Bot α] :
                                                                                instance ULift.instOrderBot {α : Type u} [LE α] [OrderBot α] :
                                                                                Equations
                                                                                  instance ULift.instOrderTop {α : Type u} [LE α] [OrderTop α] :
                                                                                  Equations
                                                                                    Equations
                                                                                      @[simp]
                                                                                      theorem bot_ne_top {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
                                                                                      @[simp]
                                                                                      theorem top_ne_bot {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
                                                                                      @[simp]
                                                                                      theorem bot_lt_top {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
                                                                                      @[simp]
                                                                                      @[simp]