⊤ 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.

Top, bottom element

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

noncomputable def topOrderOrNoTopOrder (α : Type u_1) [LE α] : OrderTop α ⊕' NoTopOrder α

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

Equations

• topOrderOrNoTopOrder α = if H : ∀ (a : α), ∃ (b : α), ¬b ≤ a then PSum.inr ⋯ else PSum.inl (OrderTop.mk ⋯)

@[simp]

theorem le_top {α : Type u} [LE α] [OrderTop α] {a : α} : a ≤ ⊤

@[simp]

theorem isTop_top {α : Type u} [LE α] [OrderTop α] : IsTop ⊤

@[simp]

theorem isMax_top {α : Type u} [Preorder α] [OrderTop α] : IsMax ⊤

@[simp]

theorem not_top_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} : ¬⊤ < a

theorem ne_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) : a ≠ ⊤

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

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 : α} : IsMax a ↔ a = ⊤

@[simp]

theorem isTop_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : IsTop a ↔ a = ⊤

theorem not_isMax_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ¬IsMax a ↔ a ≠ ⊤

theorem not_isTop_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ¬IsTop a ↔ a ≠ ⊤

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

Alias of the forward direction of isMax_iff_eq_top.

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

Alias of the forward direction of isTop_iff_eq_top.

@[simp]

theorem top_le_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ⊤ ≤ a ↔ a = ⊤

theorem top_unique {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : ⊤ ≤ a) : a = ⊤

theorem eq_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : a = ⊤ ↔ ⊤ ≤ 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 : α} : a < ⊤ ↔ a ≠ ⊤

@[simp]

theorem not_lt_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ¬a < ⊤ ↔ 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) : a ≠ ⊤

theorem top_not_mem_iff {α : Type u} [PartialOrder α] [OrderTop α] {s : Set α} : ¬⊤ ∈ s ↔ ∀ (x : α), x ∈ s → x < ⊤

theorem not_isMin_top {α : Type u} [PartialOrder α] [OrderTop α] [Nontrivial α] : ¬IsMin ⊤

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 α : 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

noncomputable def botOrderOrNoBotOrder (α : Type u_1) [LE α] : OrderBot α ⊕' NoBotOrder α

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

Equations

• botOrderOrNoBotOrder α = if H : ∀ (a : α), ∃ (b : α), ¬a ≤ b then PSum.inr ⋯ else PSum.inl (OrderBot.mk ⋯)

@[simp]

theorem bot_le {α : Type u} [LE α] [OrderBot α] {a : α} : ⊥ ≤ a

@[simp]

theorem isBot_bot {α : Type u} [LE α] [OrderBot α] : IsBot ⊥

instance OrderDual.instTop (α : Type u) [Bot α] : Top αᵒᵈ

Equations

• OrderDual.instTop α = { top := ⊥ }

instance OrderDual.instBot (α : Type u) [Top α] : Bot αᵒᵈ

Equations

• OrderDual.instBot α = { bot := ⊤ }

instance OrderDual.instOrderTop (α : Type u) [LE α] [OrderBot α] : OrderTop αᵒᵈ

Equations

• OrderDual.instOrderTop α = OrderTop.mk ⋯

instance OrderDual.instOrderBot (α : Type u) [LE α] [OrderTop α] : OrderBot αᵒᵈ

Equations

• OrderDual.instOrderBot α = OrderBot.mk ⋯

@[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 α] : IsMin ⊥

@[simp]

theorem not_lt_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} : ¬a < ⊥

theorem ne_bot_of_gt {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : a < b) : b ≠ ⊥

theorem LT.lt.ne_bot {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : a < b) : 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 : α} : IsMin a ↔ a = ⊥

@[simp]

theorem isBot_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : IsBot a ↔ a = ⊥

theorem not_isMin_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ¬IsMin a ↔ a ≠ ⊥

theorem not_isBot_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ¬IsBot a ↔ a ≠ ⊥

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

Alias of the forward direction of isMin_iff_eq_bot.

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

Alias of the forward direction of isBot_iff_eq_bot.

@[simp]

theorem le_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : a ≤ ⊥ ↔ a = ⊥

theorem bot_unique {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≤ ⊥) : a = ⊥

theorem eq_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : a = ⊥ ↔ 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 : α} : ⊥ < a ↔ a ≠ ⊥

@[simp]

theorem not_bot_lt_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ¬⊥ < a ↔ 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) : a ≠ ⊥

theorem bot_not_mem_iff {α : Type u} [PartialOrder α] [OrderBot α] {s : Set α} : ¬⊥ ∈ s ↔ ∀ (x : α), x ∈ s → ⊥ < x

theorem not_isMax_bot {α : Type u} [PartialOrder α] [OrderBot α] [Nontrivial α] : ¬IsMax ⊥

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 α : Type u

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

• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• bot : α
• bot_le : ∀ (a : α), ⊥ ≤ a

instance OrderDual.instBoundedOrder (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ

Equations

• OrderDual.instBoundedOrder α = BoundedOrder.mk

theorem OrderBot.instSubsingleton {α : Type u} [PartialOrder α] : Subsingleton (OrderBot α)

theorem OrderTop.instSubsingleton {α : Type u} [PartialOrder α] : Subsingleton (OrderTop α)

theorem BoundedOrder.instSubsingleton {α : Type u} [PartialOrder α] : Subsingleton (BoundedOrder α)

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 : ι) : ⊥ 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 : ι) : ⊤ 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

• Pi.instOrderTop = OrderTop.mk ⋯

instance Pi.instOrderBot {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → LE (α' i)] [(i : ι) → OrderBot (α' i)] : OrderBot ((i : ι) → α' i)

Equations

• Pi.instOrderBot = OrderBot.mk ⋯

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 = ⊤

theorem subsingleton_of_top_le_bot {α : Type u} [PartialOrder α] [BoundedOrder α] (h : ⊤ ≤ ⊥) : Subsingleton α

theorem subsingleton_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) : Subsingleton α

theorem subsingleton_iff_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] : ⊥ = ⊤ ↔ Subsingleton α

@[reducible, inline]

abbrev 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

• OrderTop.lift f map_le map_top = OrderTop.mk ⋯

@[reducible, inline]

abbrev 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

• OrderBot.lift f map_le map_bot = OrderBot.mk ⋯

@[reducible, inline]

abbrev 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

• BoundedOrder.lift f map_le map_top map_bot = BoundedOrder.mk

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

• Subtype.orderBot hbot = OrderBot.mk ⋯

@[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

• Subtype.orderTop htop = OrderTop.mk ⋯

@[reducible, inline]

abbrev 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

• Subtype.boundedOrder hbot htop = BoundedOrder.mk

@[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

• Prod.instTop α β = { top := (⊤, ⊤) }

instance Prod.instBot (α : Type u) (β : Type v) [Bot α] [Bot β] : Bot (α × β)

Equations

• Prod.instBot α β = { bot := (⊥, ⊥) }

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

• Prod.instOrderTop α β = OrderTop.mk ⋯

instance Prod.instOrderBot (α : Type u) (β : Type v) [LE α] [LE β] [OrderBot α] [OrderBot β] : OrderBot (α × β)

Equations

• Prod.instOrderBot α β = OrderBot.mk ⋯

instance Prod.instBoundedOrder (α : Type u) (β : Type v) [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (α × β)

Equations

• Prod.instBoundedOrder α β = BoundedOrder.mk

instance ULift.instTop {α : Type u} [Top α] : Top (ULift.{v, u} α)

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 α] : Bot (ULift.{v, u} α)

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 α] : OrderBot (ULift.{v, u} α)

Equations

• ULift.instOrderBot = OrderBot.lift ULift.down ⋯ ⋯

instance ULift.instOrderTop {α : Type u} [LE α] [OrderTop α] : OrderTop (ULift.{v, u} α)

Equations

• ULift.instOrderTop = OrderTop.lift ULift.down ⋯ ⋯

instance ULift.instBoundedOrder {α : Type u} [LE α] [BoundedOrder α] : BoundedOrder (ULift.{v, u} α)

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 α] : ⊥ < ⊤

instance Bool.instBoundedOrder : BoundedOrder Bool

Equations

• Bool.instBoundedOrder = BoundedOrder.mk

@[simp]

theorem top_eq_true : ⊤ = true

@[simp]

theorem bot_eq_false : ⊥ = false