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 #

Common lattices #

Top, bottom element #

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

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
source
noncomputable def topOrderOrNoTopOrder (α : Type u_3) [LE α] :
OrderTop α ⊕' NoTopOrder α

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

Equations
source
@[simp]
theorem le_top {α : Type u} [LE α] [OrderTop α] {a : α} :
a ≤ ⊤
source
@[simp]
theorem isTop_top {α : Type u} [LE α] [OrderTop α] :
IsTop ⊤
source
@[simp]
theorem isMax_top {α : Type u} [Preorder α] [OrderTop α] :
IsMax ⊤
source
@[simp]
theorem not_top_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} :
¬⊤ < a
source
theorem ne_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :
a ≠ ⊤
source
theorem LT.lt.ne_top {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :
a ≠ ⊤

Alias of ne_top_of_lt.

source
@[simp]
theorem isMax_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
IsMax a ↔ a = ⊤
source
@[simp]
theorem isTop_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
IsTop a ↔ a = ⊤
source
theorem not_isMax_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
¬IsMax a ↔ a ≠ ⊤
source
theorem not_isTop_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
¬IsTop a ↔ a ≠ ⊤
source
theorem IsMax.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :
IsMax a → a = ⊤

Alias of the forward direction of isMax_iff_eq_top.

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

Alias of the forward direction of isTop_iff_eq_top.

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

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
source
noncomputable def botOrderOrNoBotOrder (α : Type u_3) [LE α] :
OrderBot α ⊕' NoBotOrder α

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

Equations
source
@[simp]
theorem bot_le {α : Type u} [LE α] [OrderBot α] {a : α} :
⊥ ≤ a
source
@[simp]
theorem isBot_bot {α : Type u} [LE α] [OrderBot α] :
IsBot ⊥
source
instance OrderDual.instTop (α : Type u) [Bot α] :
Top αᵒᵈ
Equations
source
instance OrderDual.instBot (α : Type u) [Top α] :
Bot αᵒᵈ
Equations
source
instance OrderDual.instOrderTop (α : Type u) [LE α] [OrderBot α] :
OrderTop αᵒᵈ
Equations
source
instance OrderDual.instOrderBot (α : Type u) [LE α] [OrderTop α] :
OrderBot αᵒᵈ
Equations
source
@[simp]
theorem OrderDual.ofDual_bot (α : Type u) [Top α] :
OrderDual.ofDual ⊥ = ⊤
source
@[simp]
theorem OrderDual.ofDual_top (α : Type u) [Bot α] :
OrderDual.ofDual ⊤ = ⊥
source
@[simp]
theorem OrderDual.toDual_bot (α : Type u) [Bot α] :
OrderDual.toDual ⊥ = ⊤
source
@[simp]
theorem OrderDual.toDual_top (α : Type u) [Top α] :
OrderDual.toDual ⊤ = ⊥
source
@[simp]
theorem isMin_bot {α : Type u} [Preorder α] [OrderBot α] :
IsMin ⊥
source
@[simp]
theorem not_lt_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} :
¬a < ⊥
source
theorem ne_bot_of_gt {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :
b ≠ ⊥
source
theorem LT.lt.ne_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :
b ≠ ⊥

Alias of ne_bot_of_gt.

source
@[simp]
theorem isMin_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
IsMin a ↔ a = ⊥
source
@[simp]
theorem isBot_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
IsBot a ↔ a = ⊥
source
theorem not_isMin_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
¬IsMin a ↔ a ≠ ⊥
source
theorem not_isBot_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
¬IsBot a ↔ a ≠ ⊥
source
theorem IsMin.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
IsMin a → a = ⊥

Alias of the forward direction of isMin_iff_eq_bot.

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

Alias of the forward direction of isBot_iff_eq_bot.

source
@[simp]
theorem le_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
a ≤ ⊥ ↔ a = ⊥
source
theorem bot_unique {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≤ ⊥) :
a = ⊥
source
theorem eq_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
a = ⊥ ↔ a ≤ ⊥
source
theorem eq_bot_mono {α : Type u} [PartialOrder α] [OrderBot α] {a : α} {b : α} (h : a ≤ b) (h₂ : b = ⊥) :
a = ⊥
source
theorem bot_lt_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
⊥ < a ↔ a ≠ ⊥
source
@[simp]
theorem not_bot_lt_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :
¬⊥ < a ↔ a = ⊥
source
theorem eq_bot_or_bot_lt {α : Type u} [PartialOrder α] [OrderBot α] (a : α) :
a = ⊥ ∨ ⊥ < a
source
theorem eq_bot_of_minimal {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ∀ (b : α), ¬b < a) :
a = ⊥
source
theorem Ne.bot_lt {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≠ ⊥) :
⊥ < a
source
theorem Ne.bot_lt' {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ⊥ ≠ a) :
⊥ < a
source
theorem ne_bot_of_le_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hb : b ≠ ⊥) (hab : b ≤ a) :
a ≠ ⊥
source
theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) :
f a = f ⊥ ↔ a = ⊥
source
theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) :
f a = f ⊥ ↔ a = ⊥
source
theorem not_isMax_bot {α : Type u} [PartialOrder α] [OrderBot α] [Nontrivial α] :
¬IsMax ⊥
source
theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] [OrderBot β] {f : α → β} (H : StrictMono f) {a : α} (h_bot : f a = ⊥) (x : α) :
a ≤ x
source
theorem OrderBot.ext_bot {α : Type u_3} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
⊥ = ⊥
source
theorem top_sup_eq {α : Type u} [SemilatticeSup α] [OrderTop α] (a : α) :
⊤ ⊔ a = ⊤
source
theorem sup_top_eq {α : Type u} [SemilatticeSup α] [OrderTop α] (a : α) :
a ⊔ ⊤ = ⊤
source
theorem bot_sup_eq {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) :
⊥ ⊔ a = a
source
theorem sup_bot_eq {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) :
a ⊔ ⊥ = a
source
@[simp]
theorem sup_eq_bot_iff {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {b : α} :
a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
source
theorem top_inf_eq {α : Type u} [SemilatticeInf α] [OrderTop α] (a : α) :
⊤ ⊓ a = a
source
theorem inf_top_eq {α : Type u} [SemilatticeInf α] [OrderTop α] (a : α) :
a ⊓ ⊤ = a
source
@[simp]
theorem inf_eq_top_iff {α : Type u} [SemilatticeInf α] [OrderTop α] {a : α} {b : α} :
a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
source
theorem bot_inf_eq {α : Type u} [SemilatticeInf α] [OrderBot α] (a : α) :
⊥ ⊓ a = ⊥
source
theorem inf_bot_eq {α : Type u} [SemilatticeInf α] [OrderBot α] (a : α) :
a ⊓ ⊥ = ⊥

Bounded order #

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

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

    Instances
    source
    instance OrderDual.instBoundedOrder (α : Type u) [LE α] [BoundedOrder α] :
    BoundedOrder αᵒᵈ
    Equations
    source
    instance OrderBot.instSubsingleton {α : Type u} [PartialOrder α] :
    Subsingleton (OrderBot α)
    Equations
    • ⋯ = ⋯
    source
    instance OrderTop.instSubsingleton {α : Type u} [PartialOrder α] :
    Subsingleton (OrderTop α)
    Equations
    • ⋯ = ⋯
    source
    instance BoundedOrder.instSubsingleton {α : Type u} [PartialOrder α] :
    Subsingleton (BoundedOrder α)
    Equations
    • ⋯ = ⋯

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

    source
    theorem monotone_and {α : Type u} [Preorder α] {p : α → Prop} {q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :
    Monotone fun (x : α) => p x ∧ q x
    source
    theorem monotone_or {α : Type u} [Preorder α] {p : α → Prop} {q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :
    Monotone fun (x : α) => p x ∨ q x
    source
    theorem monotone_le {α : Type u} [Preorder α] {x : α} :
    Monotone fun (x_1 : α) => x ≤ x_1
    source
    theorem monotone_lt {α : Type u} [Preorder α] {x : α} :
    Monotone fun (x_1 : α) => x < x_1
    source
    theorem antitone_le {α : Type u} [Preorder α] {x : α} :
    Antitone fun (x_1 : α) => x_1 ≤ x
    source
    theorem antitone_lt {α : Type u} [Preorder α] {x : α} :
    Antitone fun (x_1 : α) => x_1 < x
    source
    theorem Monotone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) :
    Monotone fun (y : α) => ∀ (x : β), P x y
    source
    theorem Antitone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) :
    Antitone fun (y : α) => ∀ (x : β), P x y
    source
    theorem Monotone.ball {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Monotone (P x)) :
    Monotone fun (y : α) => ∀ (x : β), x ∈ s → P x y
    source
    theorem Antitone.ball {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Antitone (P x)) :
    Antitone fun (y : α) => ∀ (x : β), x ∈ s → P x y
    source
    theorem Monotone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) :
    Monotone fun (y : α) => ∃ (x : β), P x y
    source
    theorem Antitone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) :
    Antitone fun (y : α) => ∃ (x : β), P x y
    source
    theorem forall_ge_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Monotone P) :
    (∀ (x : α), x ≥ x₀ → P x) ↔ P x₀
    source
    theorem forall_le_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Antitone P) :
    (∀ (x : α), x ≤ x₀ → P x) ↔ P x₀
    source
    theorem exists_ge_and_iff_exists {α : Type u} [SemilatticeSup α] {P : α → Prop} {x₀ : α} (hP : Monotone P) :
    (∃ (x : α), x₀ ≤ x ∧ P x) ↔ ∃ (x : α), P x
    source
    theorem exists_le_and_iff_exists {α : Type u} [SemilatticeInf α] {P : α → Prop} {x₀ : α} (hP : Antitone P) :
    (∃ (x : α), x ≤ x₀ ∧ P x) ↔ ∃ (x : α), P x

    Function lattices #

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

    Pullback an OrderTop.

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

    Pullback an OrderBot.

    Equations
    source
    @[reducible]
    def BoundedOrder.lift {α : Type u} {β : Type v} [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
    BoundedOrder α

    Pullback a BoundedOrder.

    Equations

    Subtype, order dual, product lattices #

    source
    @[reducible]
    def 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
    source
    @[reducible]
    def 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
    source
    @[reducible]
    def Subtype.boundedOrder {α : Type u} {p : α → Prop} [LE α] [BoundedOrder α] (hbot : p ⊥) (htop : p ⊤) :
    BoundedOrder (Subtype p)

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

    Equations
    source
    @[simp]
    theorem Subtype.mk_bot {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) :
    { val := ⊥, property := hbot } = ⊥
    source
    @[simp]
    theorem Subtype.mk_top {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) :
    { val := ⊤, property := htop } = ⊤
    source
    theorem Subtype.coe_bot {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) :
    ↑⊥ = ⊥
    source
    theorem Subtype.coe_top {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) :
    ↑⊤ = ⊤
    source
    @[simp]
    theorem Subtype.coe_eq_bot_iff {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : { x : α // p x }} :
    ↑x = ⊥ ↔ x = ⊥
    source
    @[simp]
    theorem Subtype.coe_eq_top_iff {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : { x : α // p x }} :
    ↑x = ⊤ ↔ x = ⊤
    source
    @[simp]
    theorem Subtype.mk_eq_bot_iff {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : α} (hx : p x) :
    { val := x, property := hx } = ⊥ ↔ x = ⊥
    source
    @[simp]
    theorem Subtype.mk_eq_top_iff {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : α} (hx : p x) :
    { val := x, property := hx } = ⊤ ↔ x = ⊤
    source
    instance Prod.instTop (α : Type u) (β : Type v) [Top α] [Top β] :
    Top (α × β)
    Equations
    source
    instance Prod.instBot (α : Type u) (β : Type v) [Bot α] [Bot β] :
    Bot (α × β)
    Equations
    source
    theorem Prod.fst_top (α : Type u) (β : Type v) [Top α] [Top β] :
    ⊤.1 = ⊤
    source
    theorem Prod.snd_top (α : Type u) (β : Type v) [Top α] [Top β] :
    ⊤.2 = ⊤
    source
    theorem Prod.fst_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
    ⊥.1 = ⊥
    source
    theorem Prod.snd_bot (α : Type u) (β : Type v) [Bot α] [Bot β] :
    ⊥.2 = ⊥
    source
    instance Prod.instOrderTop (α : Type u) (β : Type v) [LE α] [LE β] [OrderTop α] [OrderTop β] :
    OrderTop (α × β)
    Equations
    source
    instance Prod.instOrderBot (α : Type u) (β : Type v) [LE α] [LE β] [OrderBot α] [OrderBot β] :
    OrderBot (α × β)
    Equations
    source
    instance Prod.instBoundedOrder (α : Type u) (β : Type v) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] :
    BoundedOrder (α × β)
    Equations
    source
    instance ULift.instTopULift {α : Type u} [Top α] :
    Top (ULift.{v, u} α)
    Equations
    • ULift.instTopULift = { top := { down := ⊤ } }
    source
    @[simp]
    theorem ULift.up_top {α : Type u} [Top α] :
    { down := ⊤ } = ⊤
    source
    @[simp]
    theorem ULift.down_top {α : Type u} [Top α] :
    ⊤.down = ⊤
    source
    instance ULift.instBotULift {α : Type u} [Bot α] :
    Bot (ULift.{v, u} α)
    Equations
    • ULift.instBotULift = { bot := { down := ⊥ } }
    source
    @[simp]
    theorem ULift.up_bot {α : Type u} [Bot α] :
    { down := ⊥ } = ⊥
    source
    @[simp]
    theorem ULift.down_bot {α : Type u} [Bot α] :
    ⊥.down = ⊥
    source
    instance ULift.instOrderBotULiftInstLEULift {α : Type u} [LE α] [OrderBot α] :
    OrderBot (ULift.{v, u} α)
    Equations
    source
    instance ULift.instOrderTopULiftInstLEULift {α : Type u} [LE α] [OrderTop α] :
    OrderTop (ULift.{v, u} α)
    Equations
    source
    instance ULift.instBoundedOrderULiftInstLEULift {α : Type u} [LE α] [BoundedOrder α] :
    BoundedOrder (ULift.{v, u} α)
    Equations
    • ULift.instBoundedOrderULiftInstLEULift = BoundedOrder.mk
    source
    theorem min_bot_left {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
    min ⊥ a = ⊥
    source
    theorem max_top_left {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
    max ⊤ a = ⊤
    source
    theorem min_top_left {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
    min ⊤ a = a
    source
    theorem max_bot_left {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
    max ⊥ a = a
    source
    theorem min_top_right {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
    min a ⊤ = a
    source
    theorem max_bot_right {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
    max a ⊥ = a
    source
    theorem min_bot_right {α : Type u} [LinearOrder α] [OrderBot α] (a : α) :
    min a ⊥ = ⊥
    source
    theorem max_top_right {α : Type u} [LinearOrder α] [OrderTop α] (a : α) :
    max a ⊤ = ⊤
    source
    @[simp]
    theorem min_eq_bot {α : Type u} [LinearOrder α] [OrderBot α] {a : α} {b : α} :
    min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
    source
    @[simp]
    theorem max_eq_top {α : Type u} [LinearOrder α] [OrderTop α] {a : α} {b : α} :
    max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
    source
    @[simp]
    theorem max_eq_bot {α : Type u} [LinearOrder α] [OrderBot α] {a : α} {b : α} :
    max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥
    source
    @[simp]
    theorem min_eq_top {α : Type u} [LinearOrder α] [OrderTop α] {a : α} {b : α} :
    min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
    source
    @[simp]
    theorem bot_ne_top {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
    ⊥ ≠ ⊤
    source
    @[simp]
    theorem top_ne_bot {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
    ⊤ ≠ ⊥
    source
    @[simp]
    theorem bot_lt_top {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] :
    ⊥ < ⊤
    source
    instance Bool.instBoundedOrder :
    BoundedOrder Bool
    Equations
    source
    @[simp]
    theorem top_eq_true :
    ⊤ = true
    source
    @[simp]
    theorem bot_eq_false :
    ⊥ = false