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
@[simp]
theorem le_top {α : Type u} [LE α] [OrderTop α] {a : α} :
@[simp]
theorem isTop_top {α : Type u} [LE α] [OrderTop α] :
@[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_not_mem_iff {α : Type u} [PartialOrder α] [OrderTop α] {s : Set α} :
¬ s ∀ (x : α), x sx <
theorem OrderTop.ext_top {α : Type u_1} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x y x y) :
noncomputable def botOrderOrNoBotOrder (α : Type u_1) [LE α] :

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

Equations
@[simp]
theorem bot_le {α : Type u} [LE α] [OrderBot α] {a : α} :
@[simp]
theorem isBot_bot {α : Type u} [LE α] [OrderBot α] :
instance OrderDual.instTop (α : Type u) [Bot α] :
Equations
instance OrderDual.instBot (α : Type u) [Top α] :
Equations
@[simp]
theorem OrderDual.ofDual_bot (α : Type u) [Top α] :
OrderDual.ofDual =
@[simp]
theorem OrderDual.ofDual_top (α : Type u) [Bot α] :
OrderDual.ofDual =
@[simp]
theorem OrderDual.toDual_bot (α : Type u) [Bot α] :
OrderDual.toDual =
@[simp]
theorem OrderDual.toDual_top (α : Type u) [Top α] :
OrderDual.toDual =
@[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_not_mem_iff {α : Type u} [PartialOrder α] [OrderBot α] {s : Set α} :
¬ s ∀ (x : α), x s < x
theorem OrderBot.ext_bot {α : Type u_1} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α) (H : ∀ (x y : α), x y x y) :

Bounded order #

Equations

Function lattices #

instance Pi.instBotForall {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Bot (α' i)] :
Bot ((i : ι) → α' i)
Equations
  • Pi.instBotForall = { bot := fun (x : ι) => }
@[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 : ι) =>
instance Pi.instTopForall {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Top (α' i)] :
Top ((i : ι) → α' i)
Equations
  • Pi.instTopForall = { top := fun (x : ι) => }
@[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 : ι) =>
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
  • Pi.instBoundedOrder = BoundedOrder.mk
theorem eq_bot_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : = ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : = ) (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
@[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
@[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

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
@[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
@[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
@[simp]
theorem Subtype.mk_bot {α : Type u} {p : αProp} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ) :
, hbot =
@[simp]
theorem Subtype.mk_top {α : Type u} {p : αProp} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ) :
, htop =
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
theorem Prod.fst_top (α : Type u) (β : Type v) [Top α] [Top β] :
.fst =
theorem Prod.snd_top (α : Type u) (β : Type v) [Top α] [Top β] :
.snd =
theorem Prod.fst_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
.fst =
theorem Prod.snd_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
.snd =
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
  • ULift.instTop = { top := { down := } }
@[simp]
theorem ULift.up_top {α : Type u} [Top α] :
{ down := } =
@[simp]
theorem ULift.down_top {α : Type u} [Top α] :
.down =
instance ULift.instBot {α : Type u} [Bot α] :
Equations
  • ULift.instBot = { bot := { down := } }
@[simp]
theorem ULift.up_bot {α : Type u} [Bot α] :
{ down := } =
@[simp]
theorem ULift.down_bot {α : Type u} [Bot α] :
.down =
instance ULift.instOrderBot {α : Type u} [LE α] [OrderBot α] :
Equations
instance ULift.instOrderTop {α : Type u} [LE α] [OrderTop α] :
Equations
Equations
  • ULift.instBoundedOrder = BoundedOrder.mk
@[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]