# Documentation

Mathlib.Order.BoundedOrder

# ⊤ 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/Bot> α: Typeclasses to declare the ⊤/⊥ notation.
• Order<Top/Bot> α: Order with a top/bottom element.
• BoundedOrder α: Order with a top and bottom element.

## Common lattices #

• Distributive lattices with a bottom element. Notated by [DistribLattice α] [OrderBot α] It captures the properties of Disjoint that are common to GeneralizedBooleanAlgebra and DistribLattice when OrderBot.
• Bounded and distributive lattice. Notated by [DistribLattice α] [BoundedOrder α]. Typical examples include Prop and Det α.

### Top, bottom element #

theorem Top.ext {α : Type u} (x : Top α) (y : Top α) (top : ) :
x = y
theorem Top.ext_iff {α : Type u} (x : Top α) (y : Top α) :
x = y
class Top (α : Type u) :

Typeclass for the ⊤ (\top) notation

• top : α

The top (⊤, \top) element

Instances
theorem Bot.ext {α : Type u} (x : Bot α) (y : Bot α) (bot : ) :
x = y
theorem Bot.ext_iff {α : Type u} (x : Bot α) (y : Bot α) :
x = y
class Bot (α : Type u) :

Typeclass for the ⊥ (\bot) notation

• bot : α

The bot (⊥, \bot) element

Instances

The top (⊤, \top) element

Equations
Instances For

The bot (⊥, \bot) element

Equations
Instances For
instance top_nonempty (α : Type u) [Top α] :
Equations
• (_ : ) = (_ : )
instance bot_nonempty (α : Type u) [Bot α] :
Equations
• (_ : ) = (_ : )
class OrderTop (α : Type u) [LE α] extends :

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_3) [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 α] [] {a : α} :
@[simp]
theorem isTop_top {α : Type u} [LE α] [] :
@[simp]
theorem isMax_top {α : Type u} [] [] :
@[simp]
theorem not_top_lt {α : Type u} [] [] {a : α} :
theorem ne_top_of_lt {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
theorem LT.lt.ne_top {α : Type u} [] [] {a : α} {b : α} (h : a < b) :

Alias of ne_top_of_lt.

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

Alias of the forward direction of isMax_iff_eq_top.

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

Alias of the forward direction of isTop_iff_eq_top.

@[simp]
theorem top_le_iff {α : Type u} [] [] {a : α} :
theorem top_unique {α : Type u} [] [] {a : α} (h : a) :
a =
theorem eq_top_iff {α : Type u} [] [] {a : α} :
theorem eq_top_mono {α : Type u} [] [] {a : α} {b : α} (h : a b) (h₂ : a = ) :
b =
theorem lt_top_iff_ne_top {α : Type u} [] [] {a : α} :
@[simp]
theorem not_lt_top_iff {α : Type u} [] [] {a : α} :
theorem eq_top_or_lt_top {α : Type u} [] [] (a : α) :
a = a <
theorem Ne.lt_top {α : Type u} [] [] {a : α} (h : a ) :
a <
theorem Ne.lt_top' {α : Type u} [] [] {a : α} (h : a) :
a <
theorem ne_top_of_le_ne_top {α : Type u} [] [] {a : α} {b : α} (hb : b ) (hab : a b) :
theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [] [] [] {f : αβ} {a : α} (hf : ) :
f a = f a =
theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [] [] [] {f : αβ} {a : α} (hf : ) :
f a = f a =
theorem not_isMin_top {α : Type u} [] [] [] :
theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [] [] [] {f : αβ} (H : ) {a : α} (h_top : f a = ) (x : α) :
x a
theorem OrderTop.ext_top {α : Type u_3} {hA : } (A : ) {hB : } (B : ) (H : ∀ (x y : α), x y x y) :
class OrderBot (α : Type u) [LE α] extends :

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_3) [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 α] [] {a : α} :
@[simp]
theorem isBot_bot {α : Type u} [LE α] [] :
instance OrderDual.top (α : Type u) [Bot α] :
Equations
instance OrderDual.bot (α : Type u) [Top α] :
Equations
instance OrderDual.orderTop (α : Type u) [LE α] [] :
Equations
instance OrderDual.orderBot (α : Type u) [LE α] [] :
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} [] [] :
@[simp]
theorem not_lt_bot {α : Type u} [] [] {a : α} :
theorem ne_bot_of_gt {α : Type u} [] [] {a : α} {b : α} (h : a < b) :
theorem LT.lt.ne_bot {α : Type u} [] [] {a : α} {b : α} (h : a < b) :

Alias of ne_bot_of_gt.

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

Alias of the forward direction of isMin_iff_eq_bot.

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

Alias of the forward direction of isBot_iff_eq_bot.

@[simp]
theorem le_bot_iff {α : Type u} [] [] {a : α} :
theorem bot_unique {α : Type u} [] [] {a : α} (h : a ) :
a =
theorem eq_bot_iff {α : Type u} [] [] {a : α} :
theorem eq_bot_mono {α : Type u} [] [] {a : α} {b : α} (h : a b) (h₂ : b = ) :
a =
theorem bot_lt_iff_ne_bot {α : Type u} [] [] {a : α} :
@[simp]
theorem not_bot_lt_iff {α : Type u} [] [] {a : α} :
theorem eq_bot_or_bot_lt {α : Type u} [] [] (a : α) :
a = < a
theorem eq_bot_of_minimal {α : Type u} [] [] {a : α} (h : ∀ (b : α), ¬b < a) :
a =
theorem Ne.bot_lt {α : Type u} [] [] {a : α} (h : a ) :
< a
theorem Ne.bot_lt' {α : Type u} [] [] {a : α} (h : a) :
< a
theorem ne_bot_of_le_ne_bot {α : Type u} [] [] {a : α} {b : α} (hb : b ) (hab : b a) :
theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [] [] [] {f : αβ} {a : α} (hf : ) :
f a = f a =
theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [] [] [] {f : αβ} {a : α} (hf : ) :
f a = f a =
theorem not_isMax_bot {α : Type u} [] [] [] :
theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [] [] [] {f : αβ} (H : ) {a : α} (h_bot : f a = ) (x : α) :
a x
theorem OrderBot.ext_bot {α : Type u_3} {hA : } (A : ) {hB : } (B : ) (H : ∀ (x y : α), x y x y) :
theorem top_sup_eq {α : Type u} [] [] {a : α} :
theorem sup_top_eq {α : Type u} [] [] {a : α} :
theorem bot_sup_eq {α : Type u} [] [] {a : α} :
a = a
theorem sup_bot_eq {α : Type u} [] [] {a : α} :
a = a
@[simp]
theorem sup_eq_bot_iff {α : Type u} [] [] {a : α} {b : α} :
a b = a = b =
theorem top_inf_eq {α : Type u} [] [] {a : α} :
a = a
theorem inf_top_eq {α : Type u} [] [] {a : α} :
a = a
@[simp]
theorem inf_eq_top_iff {α : Type u} [] [] {a : α} {b : α} :
a b = a = b =
theorem bot_inf_eq {α : Type u} [] [] {a : α} :
theorem inf_bot_eq {α : Type u} [] [] {a : α} :

### Bounded order #

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

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

Instances
instance OrderDual.boundedOrder (α : Type u) [LE α] [] :
Equations
• = let src := ; let src_1 := ; BoundedOrder.mk
instance OrderBot.instSubsingleton {α : Type u} [] :
Equations
• (_ : ) = (_ : )
instance OrderTop.instSubsingleton {α : Type u} [] :
Equations
• (_ : ) = (_ : )
instance BoundedOrder.instSubsingleton {α : Type u} [] :
Equations
• (_ : ) = (_ : )

#### In this section we prove some properties about monotone and antitone operations on Prop#

theorem monotone_and {α : Type u} [] {p : αProp} {q : αProp} (m_p : ) (m_q : ) :
Monotone fun (x : α) => p x q x
theorem monotone_or {α : Type u} [] {p : αProp} {q : αProp} (m_p : ) (m_q : ) :
Monotone fun (x : α) => p x q x
theorem monotone_le {α : Type u} [] {x : α} :
Monotone fun (x_1 : α) => x x_1
theorem monotone_lt {α : Type u} [] {x : α} :
Monotone fun (x_1 : α) => x < x_1
theorem antitone_le {α : Type u} [] {x : α} :
Antitone fun (x_1 : α) => x_1 x
theorem antitone_lt {α : Type u} [] {x : α} :
Antitone fun (x_1 : α) => x_1 < x
theorem Monotone.forall {α : Type u} {β : Type v} [] {P : βαProp} (hP : ∀ (x : β), Monotone (P x)) :
Monotone fun (y : α) => ∀ (x : β), P x y
theorem Antitone.forall {α : Type u} {β : Type v} [] {P : βαProp} (hP : ∀ (x : β), Antitone (P x)) :
Antitone fun (y : α) => ∀ (x : β), P x y
theorem Monotone.ball {α : Type u} {β : Type v} [] {P : βαProp} {s : Set β} (hP : ∀ (x : β), x sMonotone (P x)) :
Monotone fun (y : α) => ∀ (x : β), x sP x y
theorem Antitone.ball {α : Type u} {β : Type v} [] {P : βαProp} {s : Set β} (hP : ∀ (x : β), x sAntitone (P x)) :
Antitone fun (y : α) => ∀ (x : β), x sP x y
theorem Monotone.exists {α : Type u} {β : Type v} [] {P : βαProp} (hP : ∀ (x : β), Monotone (P x)) :
Monotone fun (y : α) => ∃ (x : β), P x y
theorem Antitone.exists {α : Type u} {β : Type v} [] {P : βαProp} (hP : ∀ (x : β), Antitone (P x)) :
Antitone fun (y : α) => ∃ (x : β), P x y
theorem forall_ge_iff {α : Type u} [] {P : αProp} {x₀ : α} (hP : ) :
(∀ (x : α), x x₀P x) P x₀
theorem forall_le_iff {α : Type u} [] {P : αProp} {x₀ : α} (hP : ) :
(∀ (x : α), x x₀P x) P x₀
theorem exists_ge_and_iff_exists {α : Type u} [] {P : αProp} {x₀ : α} (hP : ) :
(∃ (x : α), x₀ x P x) ∃ (x : α), P x
theorem exists_le_and_iff_exists {α : Type u} [] {P : αProp} {x₀ : α} (hP : ) :
(∃ (x : α), x x₀ P x) ∃ (x : α), P x

### Function lattices #

instance Pi.instBotForAll {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Bot (α' i)] :
Bot ((i : ι) → α' i)
Equations
• Pi.instBotForAll = { bot := fun (x : ι) => }
@[simp]
theorem Pi.bot_apply {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Bot (α' i)] (i : ι) :
theorem Pi.bot_def {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Bot (α' i)] :
= fun (x : ι) =>
instance Pi.instTopForAll {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Top (α' i)] :
Top ((i : ι) → α' i)
Equations
• Pi.instTopForAll = { top := fun (x : ι) => }
@[simp]
theorem Pi.top_apply {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Top (α' i)] (i : ι) :
theorem Pi.top_def {ι : Type u_3} {α' : ιType u_4} [(i : ι) → Top (α' i)] :
= fun (x : ι) =>
instance Pi.orderTop {ι : Type u_3} {α' : ιType u_4} [(i : ι) → LE (α' i)] [(i : ι) → OrderTop (α' i)] :
OrderTop ((i : ι) → α' i)
Equations
instance Pi.orderBot {ι : Type u_3} {α' : ιType u_4} [(i : ι) → LE (α' i)] [(i : ι) → OrderBot (α' i)] :
OrderBot ((i : ι) → α' i)
Equations
instance Pi.boundedOrder {ι : Type u_3} {α' : ιType u_4} [(i : ι) → LE (α' i)] [(i : ι) → BoundedOrder (α' i)] :
BoundedOrder ((i : ι) → α' i)
Equations
theorem eq_bot_of_bot_eq_top {α : Type u} [] [] (hα : ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u} [] [] (hα : ) (x : α) :
x =
theorem subsingleton_of_top_le_bot {α : Type u} [] [] (h : ) :
theorem subsingleton_of_bot_eq_top {α : Type u} [] [] (hα : ) :
theorem subsingleton_iff_bot_eq_top {α : Type u} [] [] :
@[reducible]
def OrderTop.lift {α : Type u} {β : Type v} [LE α] [Top α] [LE β] [] (f : αβ) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) :

Pullback an OrderTop.

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

Pullback an OrderBot.

Equations
Instances For
@[reducible]
def BoundedOrder.lift {α : Type u} {β : Type v} [LE α] [Top α] [Bot α] [LE β] [] (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]
def Subtype.orderBot {α : Type u} {p : αProp} [LE α] [] (hbot : p ) :
OrderBot { x : α // p x }

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

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

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

Equations
Instances For
@[reducible]
def Subtype.boundedOrder {α : Type u} {p : αProp} [LE α] [] (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} [] [] [OrderBot ()] (hbot : p ) :
{ val := , property := hbot } =
@[simp]
theorem Subtype.mk_top {α : Type u} {p : αProp} [] [] [OrderTop ()] (htop : p ) :
{ val := , property := htop } =
theorem Subtype.coe_bot {α : Type u} {p : αProp} [] [] [OrderBot ()] (hbot : p ) :
=
theorem Subtype.coe_top {α : Type u} {p : αProp} [] [] [OrderTop ()] (htop : p ) :
=
@[simp]
theorem Subtype.coe_eq_bot_iff {α : Type u} {p : αProp} [] [] [OrderBot ()] (hbot : p ) {x : { x : α // p x }} :
x = x =
@[simp]
theorem Subtype.coe_eq_top_iff {α : Type u} {p : αProp} [] [] [OrderTop ()] (htop : p ) {x : { x : α // p x }} :
x = x =
@[simp]
theorem Subtype.mk_eq_bot_iff {α : Type u} {p : αProp} [] [] [OrderBot ()] (hbot : p ) {x : α} (hx : p x) :
{ val := x, property := hx } = x =
@[simp]
theorem Subtype.mk_eq_top_iff {α : Type u} {p : αProp} [] [] [OrderTop ()] (htop : p ) {x : α} (hx : p x) :
{ val := x, property := hx } = x =
instance Prod.top (α : Type u) (β : Type v) [Top α] [Top β] :
Top (α × β)
Equations
instance Prod.bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
Bot (α × β)
Equations
theorem Prod.fst_top (α : Type u) (β : Type v) [Top α] [Top β] :
theorem Prod.snd_top (α : Type u) (β : Type v) [Top α] [Top β] :
theorem Prod.fst_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
theorem Prod.snd_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
instance Prod.orderTop (α : Type u) (β : Type v) [LE α] [LE β] [] [] :
OrderTop (α × β)
Equations
instance Prod.orderBot (α : Type u) (β : Type v) [LE α] [LE β] [] [] :
OrderBot (α × β)
Equations
instance Prod.boundedOrder (α : Type u) (β : Type v) [LE α] [LE β] [] [] :
Equations
instance ULift.instTopULift {α : Type u} [Top α] :
Top ()
Equations
• ULift.instTopULift = { top := { down := } }
@[simp]
theorem ULift.up_top {α : Type u} [Top α] :
{ down := } =
@[simp]
theorem ULift.down_top {α : Type u} [Top α] :
.down =
instance ULift.instBotULift {α : Type u} [Bot α] :
Bot ()
Equations
• ULift.instBotULift = { bot := { down := } }
@[simp]
theorem ULift.up_bot {α : Type u} [Bot α] :
{ down := } =
@[simp]
theorem ULift.down_bot {α : Type u} [Bot α] :
.down =
instance ULift.instOrderBotULiftInstLEULift {α : Type u} [LE α] [] :
Equations
• ULift.instOrderBotULiftInstLEULift = OrderBot.lift ULift.down (_ : ∀ (x x_1 : ), x.down x_1.downx x_1) (_ : .down = )
instance ULift.instOrderTopULiftInstLEULift {α : Type u} [LE α] [] :
Equations
• ULift.instOrderTopULiftInstLEULift = OrderTop.lift ULift.down (_ : ∀ (x x_1 : ), x.down x_1.downx x_1) (_ : .down = )
Equations
• ULift.instBoundedOrderULiftInstLEULift = BoundedOrder.mk
theorem min_bot_left {α : Type u} [] [] (a : α) :
theorem max_top_left {α : Type u} [] [] (a : α) :
theorem min_top_left {α : Type u} [] [] (a : α) :
min a = a
theorem max_bot_left {α : Type u} [] [] (a : α) :
max a = a
theorem min_top_right {α : Type u} [] [] (a : α) :
min a = a
theorem max_bot_right {α : Type u} [] [] (a : α) :
max a = a
theorem min_bot_right {α : Type u} [] [] (a : α) :
theorem max_top_right {α : Type u} [] [] (a : α) :
@[simp]
theorem min_eq_bot {α : Type u} [] [] {a : α} {b : α} :
min a b = a = b =
@[simp]
theorem max_eq_top {α : Type u} [] [] {a : α} {b : α} :
max a b = a = b =
@[simp]
theorem max_eq_bot {α : Type u} [] [] {a : α} {b : α} :
max a b = a = b =
@[simp]
theorem min_eq_top {α : Type u} [] [] {a : α} {b : α} :
min a b = a = b =
@[simp]
theorem bot_ne_top {α : Type u} [] [] [] :
@[simp]
theorem top_ne_bot {α : Type u} [] [] [] :
@[simp]
theorem bot_lt_top {α : Type u} [] [] [] :
Equations
@[simp]
theorem top_eq_true :
@[simp]
theorem bot_eq_false :