⊤ 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

• α: Typeclasses to declare the ⊤⊤/⊥⊥ notation.
• Order α: 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

ink

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

ink

theorem Top.ext_iff {α : Type u} (x : Top α) (y : Top α) : x = y ↔ ⊤ = ⊤

ink

class Top (α : Type u) : Type u

• The top (⊤⊤, \top) element

  top : α

Typeclass for the ⊤⊤ (\top) notation

ink

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

ink

theorem Bot.ext_iff {α : Type u} (x : Bot α) (y : Bot α) : x = y ↔ ⊥ = ⊥

ink

class Bot (α : Type u) : Type u

• The bot (⊥⊥, \bot) element

  bot : α

Typeclass for the ⊥⊥ (\bot) notation

ink

def «term⊤» : Lean.ParserDescr

The top (⊤⊤, \top) element

Equations

• «term⊤» = Lean.ParserDescr.node `term⊤ 1024 (Lean.ParserDescr.symbol "⊤")

ink

def «term⊥» : Lean.ParserDescr

The bot (⊥⊥, \bot) element

Equations

• «term⊥» = Lean.ParserDescr.node `term⊥ 1024 (Lean.ParserDescr.symbol "⊥")

ink

instance top_nonempty (α : Type u) [inst : Top α] : Nonempty α

Equations

• top_nonempty = top_nonempty.proof_1

ink

instance bot_nonempty (α : Type u) [inst : Bot α] : Nonempty α

Equations

• bot_nonempty = bot_nonempty.proof_1

ink

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

• ⊤⊤ is the greatest element

  le_top : ∀ (a : α), a ≤ ⊤

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.

ink

noncomputable def topOrderOrNoTopOrder (α : Type u_1) [inst : 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 (_ : NoTopOrder α) else PSum.inl (OrderTop.mk (_ : ∀ (b : α), b ≤ Classical.choose (_ : ∃ x, ∀ (a : α), a ≤ x)))

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

Alias of ne_top_of_lt.

ink

@[simp]

theorem isMax_iff_eq_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} : IsMax a ↔ a = ⊤

ink

@[simp]

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

ink

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

ink

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

ink

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

Alias of the forward direction of isMax_iff_eq_top.

ink

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

Alias of the forward direction of isTop_iff_eq_top.

ink

@[simp]

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

ink

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

ink

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

ink

theorem eq_top_mono {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (h : a ≤ b) (h₂ : a = ⊤) : b = ⊤

ink

theorem lt_top_iff_ne_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} : a < ⊤ ↔ a ≠ ⊤

ink

@[simp]

theorem not_lt_top_iff {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} : ¬a < ⊤ ↔ a = ⊤

ink

theorem eq_top_or_lt_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] (a : α) : a = ⊤ ∨ a < ⊤

ink

theorem Ne.lt_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : a ≠ ⊤) : a < ⊤

ink

theorem Ne.lt_top' {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} (h : ⊤ ≠ a) : a < ⊤

ink

theorem ne_top_of_le_ne_top {α : Type u} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (hb : b ≠ ⊤) (hab : a ≤ b) : a ≠ ⊤

ink

theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [inst : PartialOrder α] [inst : OrderTop α] [inst : Preorder β] {f : α → β} {a : α} (hf : StrictMono f) : f a = f ⊤ ↔ a = ⊤

ink

theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [inst : PartialOrder α] [inst : OrderTop α] [inst : Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) : f a = f ⊤ ↔ a = ⊤

ink

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

ink

theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [inst : LinearOrder α] [inst : Preorder β] [inst : OrderTop β] {f : α → β} (H : StrictMono f) {a : α} (h_top : f a = ⊤) (x : α) : x ≤ a

ink

theorem OrderTop.ext_top {α : Type u_1} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) : ⊤ = ⊤

ink

theorem OrderTop.ext {α : Type u_1} [inst : PartialOrder α] {A : OrderTop α} {B : OrderTop α} : A = B

ink

class OrderBot (α : Type u) [inst : LE α] extends Bot : Type u

• ⊥⊥ is the least element

  bot_le : ∀ (a : α), ⊥ ≤ a

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.

ink

noncomputable def botOrderOrNoBotOrder (α : Type u_1) [inst : 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 (_ : NoBotOrder α) else PSum.inl (OrderBot.mk (_ : ∀ (b : α), Classical.choose (_ : ∃ x, ∀ (a : α), x ≤ a) ≤ b))

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• OrderDual.orderTop α = let src := inferInstanceAs (Top αᵒᵈ); OrderTop.mk (_ : ∀ {a : α}, ⊥ ≤ a)

ink

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

Equations

• OrderDual.orderBot α = let src := inferInstanceAs (Bot αᵒᵈ); OrderBot.mk (_ : ∀ {a : α}, a ≤ ⊤)

ink

@[simp]

theorem OrderDual.ofDual_bot (α : Type u) [inst : Top α] : ↑OrderDual.ofDual ⊥ = ⊤

ink

@[simp]

theorem OrderDual.ofDual_top (α : Type u) [inst : Bot α] : ↑OrderDual.ofDual ⊤ = ⊥

ink

@[simp]

theorem OrderDual.toDual_bot (α : Type u) [inst : Bot α] : ↑OrderDual.toDual ⊥ = ⊤

ink

@[simp]

theorem OrderDual.toDual_top (α : Type u) [inst : Top α] : ↑OrderDual.toDual ⊤ = ⊥

ink

@[simp]

theorem isMin_bot {α : Type u} [inst : Preorder α] [inst : OrderBot α] : IsMin ⊥

ink

@[simp]

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

ink

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

ink

theorem LT.lt.ne_bot {α : Type u} [inst : Preorder α] [inst : OrderBot α] {a : α} {b : α} (h : a < b) : b ≠ ⊥

Alias of ne_bot_of_gt.

ink

@[simp]

theorem isMin_iff_eq_bot {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} : IsMin a ↔ a = ⊥

ink

@[simp]

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

ink

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

ink

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

ink

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

Alias of the forward direction of isMin_iff_eq_bot.

ink

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

Alias of the forward direction of isBot_iff_eq_bot.

ink

@[simp]

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

ink

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

ink

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

ink

theorem eq_bot_mono {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (h : a ≤ b) (h₂ : b = ⊥) : a = ⊥

ink

theorem bot_lt_iff_ne_bot {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} : ⊥ < a ↔ a ≠ ⊥

ink

@[simp]

theorem not_bot_lt_iff {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} : ¬⊥ < a ↔ a = ⊥

ink

theorem eq_bot_or_bot_lt {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] (a : α) : a = ⊥ ∨ ⊥ < a

ink

theorem eq_bot_of_minimal {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} (h : ∀ (b : α), ¬b < a) : a = ⊥

ink

theorem Ne.bot_lt {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} (h : a ≠ ⊥) : ⊥ < a

ink

theorem Ne.bot_lt' {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} (h : ⊥ ≠ a) : ⊥ < a

ink

theorem ne_bot_of_le_ne_bot {α : Type u} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥

ink

theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [inst : PartialOrder α] [inst : OrderBot α] [inst : Preorder β] {f : α → β} {a : α} (hf : StrictMono f) : f a = f ⊥ ↔ a = ⊥

ink

theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [inst : PartialOrder α] [inst : OrderBot α] [inst : Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) : f a = f ⊥ ↔ a = ⊥

ink

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

ink

theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [inst : LinearOrder α] [inst : PartialOrder β] [inst : OrderBot β] {f : α → β} (H : StrictMono f) {a : α} (h_bot : f a = ⊥) (x : α) : a ≤ x

ink

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

ink

theorem OrderBot.ext {α : Type u_1} [inst : PartialOrder α] {A : OrderBot α} {B : OrderBot α} : A = B

ink

theorem top_sup_eq {α : Type u} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} : ⊤ ⊔ a = ⊤

ink

theorem sup_top_eq {α : Type u} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} : a ⊔ ⊤ = ⊤

ink

theorem bot_sup_eq {α : Type u} [inst : SemilatticeSup α] [inst : OrderBot α] {a : α} : ⊥ ⊔ a = a

ink

theorem sup_bot_eq {α : Type u} [inst : SemilatticeSup α] [inst : OrderBot α] {a : α} : a ⊔ ⊥ = a

ink

@[simp]

theorem sup_eq_bot_iff {α : Type u} [inst : SemilatticeSup α] [inst : OrderBot α] {a : α} {b : α} : a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

ink

theorem top_inf_eq {α : Type u} [inst : SemilatticeInf α] [inst : OrderTop α] {a : α} : ⊤ ⊓ a = a

ink

theorem inf_top_eq {α : Type u} [inst : SemilatticeInf α] [inst : OrderTop α] {a : α} : a ⊓ ⊤ = a

ink

@[simp]

theorem inf_eq_top_iff {α : Type u} [inst : SemilatticeInf α] [inst : OrderTop α] {a : α} {b : α} : a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤

ink

theorem bot_inf_eq {α : Type u} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} : ⊥ ⊓ a = ⊥

ink

theorem inf_bot_eq {α : Type u} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} : a ⊓ ⊥ = ⊥

Bounded order

ink

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

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

ink

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

Equations

• OrderDual.boundedOrder α = let src := inferInstanceAs (OrderTop αᵒᵈ); let src_1 := inferInstanceAs (OrderBot αᵒᵈ); BoundedOrder.mk

ink

theorem BoundedOrder.ext {α : Type u_1} [inst : PartialOrder α] {A : BoundedOrder α} {B : BoundedOrder α} : A = B

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

ink

theorem monotone_and {α : Type u} [inst : Preorder α] {p : α → Prop} {q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun x => p x ∧ q x

ink

theorem monotone_or {α : Type u} [inst : Preorder α] {p : α → Prop} {q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun x => p x ∨ q x

ink

theorem monotone_le {α : Type u} [inst : Preorder α] {x : α} : Monotone ((fun x x_1 => x ≤ x_1) x)

ink

theorem monotone_lt {α : Type u} [inst : Preorder α] {x : α} : Monotone ((fun x x_1 => x < x_1) x)

ink

theorem antitone_le {α : Type u} [inst : Preorder α] {x : α} : Antitone fun x => x ≤ x

ink

theorem antitone_lt {α : Type u} [inst : Preorder α] {x : α} : Antitone fun x => x < x

ink

theorem Monotone.forall {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) : Monotone fun y => (x : β) → P x y

ink

theorem Antitone.forall {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) : Antitone fun y => (x : β) → P x y

ink

theorem Monotone.ball {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Monotone (P x)) : Monotone fun y => (x : β) → x ∈ s → P x y

ink

theorem Antitone.ball {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Antitone (P x)) : Antitone fun y => (x : β) → x ∈ s → P x y

ink

theorem exists_ge_and_iff_exists {α : Type u} [inst : SemilatticeSup α] {P : α → Prop} {x₀ : α} (hP : Monotone P) : (∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x

ink

theorem exists_le_and_iff_exists {α : Type u} [inst : SemilatticeInf α] {P : α → Prop} {x₀ : α} (hP : Antitone P) : (∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x

Function lattices

ink

instance Pi.instBotForAll {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Bot (α' i)] : Bot ((i : ι) → α' i)

Equations

• Pi.instBotForAll = { bot := fun x => ⊥ }

ink

@[simp]

theorem Pi.bot_apply {ι : Type u_2} {α' : ι → Type u_1} [inst : (i : ι) → Bot (α' i)] (i : ι) : ⊥ ((i : ι) → α' i) Pi.instBotForAll i = ⊥

ink

theorem Pi.bot_def {ι : Type u_2} {α' : ι → Type u_1} [inst : (i : ι) → Bot (α' i)] : ⊥ = fun x => ⊥

ink

instance Pi.instTopForAll {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Top (α' i)] : Top ((i : ι) → α' i)

Equations

• Pi.instTopForAll = { top := fun x => ⊤ }

ink

@[simp]

theorem Pi.top_apply {ι : Type u_2} {α' : ι → Type u_1} [inst : (i : ι) → Top (α' i)] (i : ι) : ⊤ ((i : ι) → α' i) Pi.instTopForAll i = ⊤

ink

theorem Pi.top_def {ι : Type u_2} {α' : ι → Type u_1} [inst : (i : ι) → Top (α' i)] : ⊤ = fun x => ⊤

ink

instance Pi.orderTop {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → LE (α' i)] [inst : (i : ι) → OrderTop (α' i)] : OrderTop ((i : ι) → α' i)

Equations

• Pi.orderTop = let src := inferInstanceAs (Top ((i : ι) → α' i)); OrderTop.mk (_ : ∀ (x : (i : ι) → α' i) (x_1 : ι), x x_1 ≤ ⊤)

ink

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

Equations

• Pi.orderBot = let src := inferInstanceAs (Bot ((i : ι) → α' i)); OrderBot.mk (_ : ∀ (x : (i : ι) → α' i) (x_1 : ι), ⊥ ≤ x x_1)

ink

instance Pi.boundedOrder {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → LE (α' i)] [inst : (i : ι) → BoundedOrder (α' i)] : BoundedOrder ((i : ι) → α' i)

Equations

• Pi.boundedOrder = let src := inferInstanceAs (OrderTop ((i : ι) → α' i)); let src_1 := inferInstanceAs (OrderBot ((i : ι) → α' i)); BoundedOrder.mk

ink

theorem eq_bot_of_bot_eq_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] (hα : ⊥ = ⊤) (x : α) : x = ⊥

ink

theorem eq_top_of_bot_eq_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] (hα : ⊥ = ⊤) (x : α) : x = ⊤

ink

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

ink

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

ink

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

ink

def OrderTop.lift {α : Type u} {β : Type v} [inst : LE α] [inst : Top α] [inst : LE β] [inst : 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 (_ : ∀ (a : α), a ≤ ⊤)

ink

def OrderBot.lift {α : Type u} {β : Type v} [inst : LE α] [inst : Bot α] [inst : LE β] [inst : 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 (_ : ∀ (a : α), ⊥ ≤ a)

ink

def BoundedOrder.lift {α : Type u} {β : Type v} [inst : LE α] [inst : Top α] [inst : Bot α] [inst : LE β] [inst : 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 = let src := OrderTop.lift f map_le map_top; let src_1 := OrderBot.lift f map_le map_bot; BoundedOrder.mk

Subtype, order dual, product lattices

ink

def Subtype.orderBot {α : Type u} {p : α → Prop} [inst : LE α] [inst : OrderBot α] (hbot : p ⊥) : OrderBot { x // p x }

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

Equations

• Subtype.orderBot hbot = OrderBot.mk (_ : ∀ (x : { x // p x }), ⊥ ≤ ↑x)

ink

def Subtype.orderTop {α : Type u} {p : α → Prop} [inst : LE α] [inst : OrderTop α] (htop : p ⊤) : OrderTop { x // p x }

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

Equations

• Subtype.orderTop htop = OrderTop.mk (_ : ∀ (x : { x // p x }), ↑x ≤ ⊤)

ink

def Subtype.boundedOrder {α : Type u} {p : α → Prop} [inst : LE α] [inst : 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 = let src := Subtype.orderTop htop; let src_1 := Subtype.orderBot hbot; BoundedOrder.mk

ink

@[simp]

theorem Subtype.mk_bot {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ⊥) : { val := ⊥, property := hbot } = ⊥

ink

@[simp]

theorem Subtype.mk_top {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ⊤) : { val := ⊤, property := htop } = ⊤

ink

theorem Subtype.coe_bot {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ⊥) : ↑⊥ = ⊥

ink

theorem Subtype.coe_top {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ⊤) : ↑⊤ = ⊤

ink

@[simp]

theorem Subtype.coe_eq_bot_iff {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ⊥) {x : { x // p x }} : ↑x = ⊥ ↔ x = ⊥

ink

@[simp]

theorem Subtype.coe_eq_top_iff {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ⊤) {x : { x // p x }} : ↑x = ⊤ ↔ x = ⊤

ink

@[simp]

theorem Subtype.mk_eq_bot_iff {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderBot α] [inst : OrderBot (Subtype p)] (hbot : p ⊥) {x : α} (hx : p x) : { val := x, property := hx } = ⊥ ↔ x = ⊥

ink

@[simp]

theorem Subtype.mk_eq_top_iff {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst : OrderTop α] [inst : OrderTop (Subtype p)] (htop : p ⊤) {x : α} (hx : p x) : { val := x, property := hx } = ⊤ ↔ x = ⊤

ink

instance Prod.top (α : Type u) (β : Type v) [inst : Top α] [inst : Top β] : Top (α × β)

Equations

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

ink

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

Equations

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

ink

instance Prod.orderTop (α : Type u) (β : Type v) [inst : LE α] [inst : LE β] [inst : OrderTop α] [inst : OrderTop β] : OrderTop (α × β)

Equations

• Prod.orderTop α β = let src := inferInstanceAs (Top (α × β)); OrderTop.mk (_ : ∀ (x : α × β), x.fst ≤ ⊤.fst ∧ x.snd ≤ ⊤.snd)

ink

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

Equations

• Prod.orderBot α β = let src := inferInstanceAs (Bot (α × β)); OrderBot.mk (_ : ∀ (x : α × β), ⊥.fst ≤ x.fst ∧ ⊥.snd ≤ x.snd)

ink

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

Equations

• Prod.boundedOrder α β = let src := inferInstanceAs (OrderTop (α × β)); let src_1 := inferInstanceAs (OrderBot (α × β)); BoundedOrder.mk

ink

theorem min_bot_left {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) : min ⊥ a = ⊥

ink

theorem max_top_left {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) : max ⊤ a = ⊤

ink

theorem min_top_left {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) : min ⊤ a = a

ink

theorem max_bot_left {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) : max ⊥ a = a

ink

theorem min_top_right {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) : min a ⊤ = a

ink

theorem max_bot_right {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) : max a ⊥ = a

ink

theorem min_bot_right {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] (a : α) : min a ⊥ = ⊥

ink

theorem max_top_right {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] (a : α) : max a ⊤ = ⊤

ink

@[simp]

theorem min_eq_bot {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] {a : α} {b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

ink

@[simp]

theorem max_eq_top {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] {a : α} {b : α} : max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤

ink

@[simp]

theorem max_eq_bot {α : Type u} [inst : LinearOrder α] [inst : OrderBot α] {a : α} {b : α} : max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥

ink

@[simp]

theorem min_eq_top {α : Type u} [inst : LinearOrder α] [inst : OrderTop α] {a : α} {b : α} : min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤

ink

@[simp]

theorem bot_ne_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : Nontrivial α] : ⊥ ≠ ⊤

ink

@[simp]

theorem top_ne_bot {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : Nontrivial α] : ⊤ ≠ ⊥

ink

@[simp]

theorem bot_lt_top {α : Type u} [inst : PartialOrder α] [inst : BoundedOrder α] [inst : Nontrivial α] : ⊥ < ⊤

ink

instance Bool.boundedOrder : BoundedOrder Bool

Equations

• Bool.boundedOrder = BoundedOrder.mk

ink

@[simp]

theorem top_eq_true : ⊤ = true

ink

@[simp]

theorem bot_eq_false : ⊥ = false