Mathlib.Order.BoundedOrder.Basic

OrderTop structure

(α : Type u) [LE α] extends Top α

Full source

/-- 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. -/
class OrderTop (α : Type u) [LE α] extends Top α where
  /-- `⊤` is the greatest element -/
  le_top : ∀ a : α, a ≤ ⊤

Order with a top element

Informal description

An order `(α, ≤)` is called an `OrderTop` if it has a greatest element, denoted by `⊤`, such that for every element `a ∈ α`, we have `a ≤ ⊤`. This is formalized as a structure extending the `Top` typeclass, which provides the notation `⊤` for the greatest element.

topOrderOrNoTopOrder definition

(α : Type*) [LE α] : OrderTop α ⊕' NoTopOrder α

Full source

/-- An order is (noncomputably) either an `OrderTop` or a `NoTopOrder`. Use as
`casesI topOrderOrNoTopOrder α`. -/
noncomputable def topOrderOrNoTopOrder (α : Type*) [LE α] : OrderTopOrderTop α ⊕' NoTopOrder α := by
  by_cases H : ∀ a : α, ∃ b, ¬b ≤ a
  · exact PSum.inr ⟨H⟩
  · push_neg at H
    letI : Top α := ⟨Classical.choose H⟩
    exact PSum.inl ⟨Classical.choose_spec H⟩

Classification of orders with or without a top element

Informal description

For any ordered type $\alpha$, the definition `topOrderOrNoTopOrder` nonconstructively determines whether $\alpha$ has a greatest element (forming an `OrderTop`) or has no greatest element (forming a `NoTopOrder`). This is done by checking if for every element $a \in \alpha$, there exists an element $b \in \alpha$ such that $b \not\leq a$. If this condition holds for all $a$, then $\alpha$ is a `NoTopOrder`; otherwise, it is an `OrderTop` with the greatest element being the witness of the negation of the condition.

le_top theorem

: a ≤ ⊤

Full source

@[simp]
theorem le_top : a ≤ ⊤ :=
  OrderTop.le_top a

Every element is less than or equal to the top element

Informal description

For any element $a$ in a type $\alpha$ with an order and a greatest element $\top$, we have $a \leq \top$.

isTop_top theorem

: IsTop (⊤ : α)

Full source

@[simp]
theorem isTop_top : IsTop (⊤ : α) := fun _ => le_top

Top Element Property: $\top$ is a greatest element

Informal description

The greatest element $\top$ in an ordered type $\alpha$ is a top element, meaning that for any element $a \in \alpha$, we have $a \leq \top$.

IsTop.rec definition

[LE α] {P : (x : α) → IsTop x → Sort*} (h : ∀ [OrderTop α], P ⊤ isTop_top) (x : α) (hx : IsTop x) : P x hx

Full source

/-- A top element can be replaced with `⊤`.

Prefer `IsTop.eq_top` if `α` already has a top element. -/
@[elab_as_elim]
protected def IsTop.rec [LE α] {P : (x : α) → IsTop x → Sort*}
    (h : ∀ [OrderTop α], P ⊤ isTop_top) (x : α) (hx : IsTop x) : P x hx := by
  letI : OrderTop α := { top := x, le_top := hx }
  apply h

Recursion principle for top elements

Informal description

Given a type $\alpha$ with a partial order and a predicate `P` that depends on an element of $\alpha$ and a proof that it is a top element, if `P` holds for the greatest element $\top$ in any `OrderTop` instance of $\alpha$, then `P` holds for any top element $x$ in $\alpha$ with proof $hx$.

isMax_top theorem

: IsMax (⊤ : α)

Full source

@[simp]
theorem isMax_top : IsMax (⊤ : α) :=
  isTop_top.isMax

Maximality of the Top Element: $\top$ is maximal

Informal description

The greatest element $\top$ in an ordered type $\alpha$ is a maximal element, meaning there is no element $a \in \alpha$ such that $\top < a$.

not_top_lt theorem

: ¬⊤ < a

Full source

@[simp]
theorem not_top_lt : ¬⊤ < a :=
  isMax_top.not_lt

No Element is Greater Than Top: $\neg (\top < a)$

Informal description

For any element $a$ in an ordered type with a greatest element $\top$, it is not the case that $\top < a$.

ne_top_of_lt theorem

(h : a < b) : a ≠ ⊤

Full source

theorem ne_top_of_lt (h : a < b) : a ≠ ⊤ :=
  (h.trans_le le_top).ne

Strict Inequality Implies Not Top

Informal description

For any elements $a$ and $b$ in an ordered type with a greatest element $\top$, if $a < b$, then $a$ is not equal to $\top$.

lt_top_of_lt theorem

(h : a < b) : a < ⊤

Full source

theorem lt_top_of_lt (h : a < b) : a < ⊤ :=
  lt_of_lt_of_le h le_top

Strict Inequality Implies Less Than Top

Informal description

For any elements $a$ and $b$ in an ordered type with a greatest element $\top$, if $a < b$, then $a < \top$.

isMax_iff_eq_top theorem

: IsMax a ↔ a = ⊤

Full source

@[simp]
theorem isMax_iff_eq_top : IsMaxIsMax a ↔ a = ⊤ :=
  ⟨fun h => h.eq_of_le le_top, fun h _ _ => h.symm ▸ le_top⟩

Characterization of Maximal Elements as Top Element

Informal description

An element $a$ in an ordered type with a greatest element $\top$ is maximal if and only if it equals $\top$, i.e., $\text{IsMax}(a) \leftrightarrow a = \top$.

isTop_iff_eq_top theorem

: IsTop a ↔ a = ⊤

Full source

@[simp]
theorem isTop_iff_eq_top : IsTopIsTop a ↔ a = ⊤ :=
  ⟨fun h => h.isMax.eq_of_le le_top, fun h _ => h.symm ▸ le_top⟩

Characterization of Greatest Element as Top Element

Informal description

An element $a$ in an ordered type with a greatest element $\top$ is the greatest element if and only if it equals $\top$, i.e., $\text{IsTop}(a) \leftrightarrow a = \top$.

not_isMax_iff_ne_top theorem

: ¬IsMax a ↔ a ≠ ⊤

Full source

theorem not_isMax_iff_ne_top : ¬IsMax a¬IsMax a ↔ a ≠ ⊤ :=
  isMax_iff_eq_top.not

Non-maximality Characterization: $\neg \text{IsMax}(a) \leftrightarrow a \neq \top$

Informal description

An element $a$ in an ordered type with a greatest element $\top$ is not maximal if and only if it is not equal to $\top$, i.e., $\neg \text{IsMax}(a) \leftrightarrow a \neq \top$.

not_isTop_iff_ne_top theorem

: ¬IsTop a ↔ a ≠ ⊤

Full source

theorem not_isTop_iff_ne_top : ¬IsTop a¬IsTop a ↔ a ≠ ⊤ :=
  isTop_iff_eq_top.not

Non-top Element Characterization: $\neg\text{IsTop}(a) \leftrightarrow a \neq \top$

Informal description

An element $a$ in an ordered type with a greatest element $\top$ is not the greatest element if and only if $a \neq \top$, i.e., $\neg\text{IsTop}(a) \leftrightarrow a \neq \top$.

top_le_iff theorem

: ⊤ ≤ a ↔ a = ⊤

Full source

@[simp]
theorem top_le_iff : ⊤⊤ ≤ a ↔ a = ⊤ :=
  le_top.le_iff_eq.trans eq_comm

Characterization of Top Element: $\top \leq a \leftrightarrow a = \top$

Informal description

For any element $a$ in a type $\alpha$ with an order and a greatest element $\top$, the inequality $\top \leq a$ holds if and only if $a = \top$.

top_unique theorem

(h : ⊤ ≤ a) : a = ⊤

Full source

theorem top_unique (h : ⊤ ≤ a) : a = ⊤ :=
  le_top.antisymm h

Uniqueness of Top Element: $\top \leq a \Rightarrow a = \top$

Informal description

For any element $a$ in a type $\alpha$ with an order and a greatest element $\top$, if $\top \leq a$, then $a = \top$.

lt_top_iff_ne_top theorem

: a < ⊤ ↔ a ≠ ⊤

Full source

theorem lt_top_iff_ne_top : a < ⊤ ↔ a ≠ ⊤ :=
  le_top.lt_iff_ne

Strictly Less Than Top Element Characterization: $a < \top \leftrightarrow a \neq \top$

Informal description

For any element $a$ in a type $\alpha$ with a top element $\top$ and an order, $a$ is strictly less than $\top$ if and only if $a$ is not equal to $\top$.

not_lt_top_iff theorem

: ¬a < ⊤ ↔ a = ⊤

Full source

@[simp]
theorem not_lt_top_iff : ¬a < ⊤¬a < ⊤ ↔ a = ⊤ :=
  lt_top_iff_ne_top.not_left

Characterization of Elements Not Strictly Less Than Top: $\neg (a < \top) \leftrightarrow a = \top$

Informal description

For any element $a$ in a type $\alpha$ with a top element $\top$ and an order, $a$ is not strictly less than $\top$ if and only if $a$ is equal to $\top$.

Ne.lt_top theorem

(h : a ≠ ⊤) : a < ⊤

Full source

@[aesop (rule_sets := [finiteness]) safe apply]
theorem Ne.lt_top (h : a ≠ ⊤) : a < ⊤ :=
  lt_top_iff_ne_top.mpr h

Non-Top Elements are Strictly Below Top: $a \neq \top \to a < \top$

Informal description

For any element $a$ in a type $\alpha$ with a top element $\top$ and an order, if $a \neq \top$, then $a < \top$.

Ne.lt_top' theorem

(h : ⊤ ≠ a) : a < ⊤

Full source

theorem Ne.lt_top' (h : ⊤⊤ ≠ a) : a < ⊤ :=
  h.symm.lt_top

Non-Top Elements are Strictly Below Top (Symmetric Version): $\top \neq a \to a < \top$

Informal description

For any element $a$ in a type $\alpha$ with a top element $\top$ and an order, if $\top \neq a$, then $a < \top$.

ne_top_of_le_ne_top theorem

(hb : b ≠ ⊤) (hab : a ≤ b) : a ≠ ⊤

Full source

theorem ne_top_of_le_ne_top (hb : b ≠ ⊤) (hab : a ≤ b) : a ≠ ⊤ :=
  (hab.trans_lt hb.lt_top).ne

Non-Top Elements Preserve Non-Topness Under Order: $b \neq \top \land a \leq b \to a \neq \top$

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with a top element $\top$ and an order, if $b \neq \top$ and $a \leq b$, then $a \neq \top$.

top_not_mem_iff theorem

{s : Set α} : ⊤ ∉ s ↔ ∀ x ∈ s, x < ⊤

Full source

lemma top_not_mem_iff {s : Set α} : ⊤⊤ ∉ s⊤ ∉ s ↔ ∀ x ∈ s, x < ⊤ :=
  ⟨fun h x hx ↦ Ne.lt_top (fun hx' : x = ⊤ ↦ h (hx' ▸ hx)), fun h h₀ ↦ (h ⊤ h₀).false⟩

Characterization of Sets Excluding the Top Element: $\top \notin s \leftrightarrow \forall x \in s, x < \top$

Informal description

For any subset $s$ of a type $\alpha$ with a top element $\top$, the top element is not in $s$ if and only if every element $x \in s$ is strictly less than $\top$.

not_isMin_top theorem

: ¬IsMin (⊤ : α)

Full source

theorem not_isMin_top : ¬IsMin (⊤ : α) := fun h =>
  let ⟨_, ha⟩ := exists_ne (⊤ : α)
  ha <| top_le_iff.1 <| h le_top

Top Element is Not Minimal in a Partially Ordered Set

Informal description

In a partially ordered set $\alpha$ with a greatest element $\top$, the element $\top$ is not a minimal element. That is, there does not exist an element $x \in \alpha$ such that $x \leq \top$ and $x \neq \top$.

OrderTop.ext_top theorem

 {α} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α)
  (H :
    ∀ x y : α,
      (haveI := hA;
        x ≤ y) ↔
        x ≤ y) :
  (@Top.top α (@OrderTop.toTop α hA.toLE A)) = (@Top.top α (@OrderTop.toTop α hB.toLE B))

Full source

theorem OrderTop.ext_top {α} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α}
    (B : OrderTop α) (H : ∀ x y : α, (haveI := hA; x ≤ y) ↔ x ≤ y) :
    (@Top.top α (@OrderTop.toTop α hA.toLE A)) = (@Top.top α (@OrderTop.toTop α hB.toLE B)) := by
  cases PartialOrder.ext H
  apply top_unique
  exact @le_top _ _ A _

Uniqueness of Top Element in Equivalent Order Structures

Informal description

Let $\alpha$ be a type with two partial orders $h_A$ and $h_B$, each equipped with a greatest element $\top$ (via structures $A$ and $B$ of type `OrderTop`). If the two partial orders agree on all pairs of elements (i.e., for all $x, y \in \alpha$, $x \leq y$ under $h_A$ if and only if $x \leq y$ under $h_B$), then the top elements defined by $A$ and $B$ are equal: $\top_A = \top_B$.

OrderBot structure

(α : Type u) [LE α] extends Bot α

Full source

/-- 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. -/
class OrderBot (α : Type u) [LE α] extends Bot α where
  /-- `⊥` is the least element -/
  bot_le : ∀ a : α, ⊥ ≤ a

Order with a bottom element

Informal description

An order `α` with a least element `⊥` is called an `OrderBot`. This structure extends the `Bot` typeclass, which provides the notation `⊥` for the least element, and ensures that `⊥` is indeed the least element in the order, i.e., for any element `a` in `α`, we have `⊥ ≤ a`.

botOrderOrNoBotOrder definition

(α : Type*) [LE α] : OrderBot α ⊕' NoBotOrder α

Full source

/-- An order is (noncomputably) either an `OrderBot` or a `NoBotOrder`. Use as
`casesI botOrderOrNoBotOrder α`. -/
noncomputable def botOrderOrNoBotOrder (α : Type*) [LE α] : OrderBotOrderBot α ⊕' NoBotOrder α := by
  by_cases H : ∀ a : α, ∃ b, ¬a ≤ b
  · exact PSum.inr ⟨H⟩
  · push_neg at H
    letI : Bot α := ⟨Classical.choose H⟩
    exact PSum.inl ⟨Classical.choose_spec H⟩

Decomposition of ordered types into those with/without a bottom element

Informal description

For any ordered type `α`, the type is either an `OrderBot` (has a least element `⊥`) or a `NoBotOrder` (has no least element). This is a noncomputable definition that cases on whether there exists an element `a` such that for all `b`, `a ≤ b` holds.

bot_le theorem

: ⊥ ≤ a

Full source

@[simp]
theorem bot_le : ⊥ ≤ a :=
  OrderBot.bot_le a

Bottom Element is Least Element

Informal description

For any element $a$ in an order with a bottom element $\bot$, we have $\bot \leq a$.

isBot_bot theorem

: IsBot (⊥ : α)

Full source

@[simp]
theorem isBot_bot : IsBot (⊥ : α) := fun _ => bot_le

Bottom Element is Least Element

Informal description

The bottom element $\bot$ in an ordered type $\alpha$ is a least element, meaning it satisfies the property of being less than or equal to all other elements in $\alpha$.

IsBot.rec definition

[LE α] {P : (x : α) → IsBot x → Sort*} (h : ∀ [OrderBot α], P ⊥ isBot_bot) (x : α) (hx : IsBot x) : P x hx

Full source

/-- A bottom element can be replaced with `⊥`.

Prefer `IsBot.eq_bot` if `α` already has a bottom element. -/
@[elab_as_elim]
protected def IsBot.rec [LE α] {P : (x : α) → IsBot x → Sort*}
    (h : ∀ [OrderBot α], P ⊥ isBot_bot) (x : α) (hx : IsBot x) : P x hx := by
  letI : OrderBot α := { bot := x, bot_le := hx }
  apply h

Recursion Principle for Bottom Elements

Informal description

Given a type $\alpha$ with a partial order, a predicate $P$ on elements of $\alpha$ and their proofs of being a bottom element, and a proof that $P$ holds for the bottom element $\bot$ in any order with a bottom element, then $P$ holds for any element $x$ in $\alpha$ that is a bottom element (i.e., $x \leq y$ for all $y \in \alpha$).

OrderDual.instTop instance

[Bot α] : Top αᵒᵈ

Full source

instance instTop [Bot α] : Top αᵒᵈ :=
  ⟨(⊥ : α)⟩

Order Dual of a Type with Bottom Element has Top Element

Informal description

For any type $\alpha$ with a bottom element $\bot$, the order dual $\alpha^{\text{op}}$ has a top element $\top$.

OrderDual.instBot instance

[Top α] : Bot αᵒᵈ

Full source

instance instBot [Top α] : Bot αᵒᵈ :=
  ⟨(⊤ : α)⟩

Bottom Element in Order Dual of a Type with Top Element

Informal description

For any type $\alpha$ with a top element $\top$, the order dual $\alpha^{\text{op}}$ has a bottom element $\bot$.

OrderDual.instOrderTop instance

[LE α] [OrderBot α] : OrderTop αᵒᵈ

Full source

instance instOrderTop [LE α] [OrderBot α] : OrderTop αᵒᵈ where
  __ := inferInstanceAs (Top αᵒᵈ)
  le_top := @bot_le α _ _

Order Dual of a Type with Bottom Element has a Top Element

Informal description

For any ordered type $\alpha$ with a least element $\bot$, the order dual $\alpha^{\text{op}}$ has a greatest element $\top$.

OrderDual.instOrderBot instance

[LE α] [OrderTop α] : OrderBot αᵒᵈ

Full source

instance instOrderBot [LE α] [OrderTop α] : OrderBot αᵒᵈ where
  __ := inferInstanceAs (Bot αᵒᵈ)
  bot_le := @le_top α _ _

Order Dual of a Type with Top Element has a Bottom Element

Informal description

For any ordered type $\alpha$ with a greatest element $\top$, the order dual $\alpha^{\text{op}}$ has a least element $\bot$.

OrderDual.ofDual_bot theorem

[Top α] : ofDual ⊥ = (⊤ : α)

Full source

@[simp]
theorem ofDual_bot [Top α] : ofDual ⊥ = (⊤ : α) :=
  rfl

Order Dual Bottom Element Maps to Top Element: $\text{ofDual}(\bot) = \top$

Informal description

For any type $\alpha$ with a top element $\top$, the image of the bottom element $\bot$ under the order dual isomorphism `ofDual` is equal to $\top$ in $\alpha$.

OrderDual.ofDual_top theorem

[Bot α] : ofDual ⊤ = (⊥ : α)

Full source

@[simp]
theorem ofDual_top [Bot α] : ofDual ⊤ = (⊥ : α) :=
  rfl

Conversion of Top Element in Order Dual to Bottom Element in Original Type

Informal description

For any type $\alpha$ with a bottom element $\bot$, the conversion from the order dual $\alpha^{\text{op}}$ back to $\alpha$ maps the top element $\top$ in $\alpha^{\text{op}}$ to the bottom element $\bot$ in $\alpha$. That is, $\text{ofDual}(\top) = \bot$.

OrderDual.toDual_bot theorem

[Bot α] : toDual (⊥ : α) = ⊤

Full source

@[simp]
theorem toDual_bot [Bot α] : toDual (⊥ : α) = ⊤ :=
  rfl

Order Dual Maps Bottom to Top

Informal description

For any type $\alpha$ with a bottom element $\bot$, the order dual map `toDual` sends $\bot$ to the top element $\top$ of the order dual $\alpha^{\text{op}}$. That is, $\text{toDual}(\bot) = \top$.

OrderDual.toDual_top theorem

[Top α] : toDual (⊤ : α) = ⊥

Full source

@[simp]
theorem toDual_top [Top α] : toDual (⊤ : α) = ⊥ :=
  rfl

Dualization of Top Element: $\text{toDual}(\top) = \bot$ in Order Dual

Informal description

For any type $\alpha$ with a top element $\top$, the order dual $\alpha^{\text{op}}$ satisfies $\text{toDual}(\top) = \bot$, where $\text{toDual}$ is the canonical map from $\alpha$ to its order dual $\alpha^{\text{op}}$.

isMin_bot theorem

: IsMin (⊥ : α)

Full source

@[simp]
theorem isMin_bot : IsMin (⊥ : α) :=
  isBot_bot.isMin

Bottom Element is Minimal

Informal description

The bottom element $\bot$ in an ordered type $\alpha$ is a minimal element, meaning there is no element strictly less than $\bot$.

not_lt_bot theorem

: ¬a < ⊥

Full source

@[simp]
theorem not_lt_bot : ¬a < ⊥ :=
  isMin_bot.not_lt

No Element is Less Than Bottom: $\neg (a < \bot)$

Informal description

For any element $a$ in an ordered type $\alpha$ with a bottom element $\bot$, it is not the case that $a$ is strictly less than $\bot$.

ne_bot_of_gt theorem

(h : a < b) : b ≠ ⊥

Full source

theorem ne_bot_of_gt (h : a < b) : b ≠ ⊥ :=
  (bot_le.trans_lt h).ne'

Non-bottom elements are greater than bottom: $a < b \implies b \neq \bot$

Informal description

For any elements $a$ and $b$ in an order with a bottom element $\bot$, if $a < b$, then $b$ is not equal to $\bot$.

bot_lt_of_lt theorem

(h : a < b) : ⊥ < b

Full source

theorem bot_lt_of_lt (h : a < b) : ⊥ < b :=
  lt_of_le_of_lt bot_le h

Bottom Element is Less Than Any Non-Bottom Element: $a < b \implies \bot < b$

Informal description

For any elements $a$ and $b$ in an order with a bottom element $\bot$, if $a < b$, then $\bot < b$.

isMin_iff_eq_bot theorem

: IsMin a ↔ a = ⊥

Full source

@[simp]
theorem isMin_iff_eq_bot : IsMinIsMin a ↔ a = ⊥ :=
  ⟨fun h => h.eq_of_ge bot_le, fun h _ _ => h.symm ▸ bot_le⟩

Minimal Element Characterization: $a$ is minimal iff $a = \bot$

Informal description

An element $a$ is minimal in an order with a bottom element $\bot$ if and only if $a = \bot$.

isBot_iff_eq_bot theorem

: IsBot a ↔ a = ⊥

Full source

@[simp]
theorem isBot_iff_eq_bot : IsBotIsBot a ↔ a = ⊥ :=
  ⟨fun h => h.isMin.eq_of_ge bot_le, fun h _ => h.symm ▸ bot_le⟩

Characterization of Bottom Element: $a$ is least iff $a = \bot$

Informal description

An element $a$ is the bottom element (i.e., is a least element) in an order if and only if $a = \bot$.

not_isMin_iff_ne_bot theorem

: ¬IsMin a ↔ a ≠ ⊥

Full source

theorem not_isMin_iff_ne_bot : ¬IsMin a¬IsMin a ↔ a ≠ ⊥ :=
  isMin_iff_eq_bot.not

Non-minimal Element Characterization: $a$ is not minimal iff $a \neq \bot$

Informal description

An element $a$ is not minimal in an order with a bottom element $\bot$ if and only if $a \neq \bot$.

not_isBot_iff_ne_bot theorem

: ¬IsBot a ↔ a ≠ ⊥

Full source

theorem not_isBot_iff_ne_bot : ¬IsBot a¬IsBot a ↔ a ≠ ⊥ :=
  isBot_iff_eq_bot.not

Characterization of Non-Bottom Elements: $a$ is not least iff $a \neq \bot$

Informal description

An element $a$ is not the bottom element if and only if $a \neq \bot$.

le_bot_iff theorem

: a ≤ ⊥ ↔ a = ⊥

Full source

@[simp]
theorem le_bot_iff : a ≤ ⊥ ↔ a = ⊥ :=
  bot_le.le_iff_eq

Characterization of Bottom Element: $a \leq \bot \leftrightarrow a = \bot$

Informal description

For any element $a$ in an order with a bottom element $\bot$, the inequality $a \leq \bot$ holds if and only if $a = \bot$.

bot_unique theorem

(h : a ≤ ⊥) : a = ⊥

Full source

theorem bot_unique (h : a ≤ ⊥) : a = ⊥ :=
  h.antisymm bot_le

Uniqueness of Bottom Element: $a \leq \bot \Rightarrow a = \bot$

Informal description

For any element $a$ in an order with a bottom element $\bot$, if $a \leq \bot$, then $a = \bot$.

bot_lt_iff_ne_bot theorem

: ⊥ < a ↔ a ≠ ⊥

Full source

theorem bot_lt_iff_ne_bot : ⊥⊥ < a ↔ a ≠ ⊥ :=
  bot_le.lt_iff_ne.trans ne_comm

Strictly Greater Than Bottom Element Characterization

Informal description

For any element $a$ in an order with a bottom element $\bot$, the bottom element is strictly less than $a$ if and only if $a$ is not equal to the bottom element, i.e., $\bot < a \leftrightarrow a \neq \bot$.

not_bot_lt_iff theorem

: ¬⊥ < a ↔ a = ⊥

Full source

@[simp]
theorem not_bot_lt_iff : ¬⊥ < a¬⊥ < a ↔ a = ⊥ :=
  bot_lt_iff_ne_bot.not_left

Characterization of Elements Not Greater Than Bottom

Informal description

For any element $a$ in an order with a bottom element $\bot$, the bottom element is not strictly less than $a$ if and only if $a$ is equal to $\bot$, i.e., $\neg(\bot < a) \leftrightarrow a = \bot$.

Ne.bot_lt theorem

(h : a ≠ ⊥) : ⊥ < a

Full source

theorem Ne.bot_lt (h : a ≠ ⊥) : ⊥ < a :=
  bot_lt_iff_ne_bot.mpr h

Bottom Element is Strictly Less Than Any Non-Bottom Element

Informal description

For any element $a$ in an order with a bottom element $\bot$, if $a$ is not equal to $\bot$, then $\bot$ is strictly less than $a$, i.e., $a \neq \bot \implies \bot < a$.

Ne.bot_lt' theorem

(h : ⊥ ≠ a) : ⊥ < a

Full source

theorem Ne.bot_lt' (h : ⊥⊥ ≠ a) : ⊥ < a :=
  h.symm.bot_lt

Bottom Element is Strictly Less Than Any Non-Bottom Element (Symmetric Version)

Informal description

For any element $a$ in an order with a bottom element $\bot$, if $\bot$ is not equal to $a$, then $\bot$ is strictly less than $a$, i.e., $\bot \neq a \implies \bot < a$.

ne_bot_of_le_ne_bot theorem

(hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥

Full source

theorem ne_bot_of_le_ne_bot (hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥ :=
  (hb.bot_lt.trans_le hab).ne'

Non-Bottom Elements are Upward-Closed with Respect to Bottom

Informal description

For any elements $a$ and $b$ in an order with a bottom element $\bot$, if $b \neq \bot$ and $b \leq a$, then $a \neq \bot$.

bot_not_mem_iff theorem

{s : Set α} : ⊥ ∉ s ↔ ∀ x ∈ s, ⊥ < x

Full source

lemma bot_not_mem_iff {s : Set α} : ⊥⊥ ∉ s⊥ ∉ s ↔ ∀ x ∈ s, ⊥ < x :=
  top_not_mem_iff (α := αᵒᵈ)

Characterization of Sets Excluding the Bottom Element: $\bot \notin s \leftrightarrow \forall x \in s, \bot < x$

Informal description

For any subset $s$ of a type $\alpha$ with a bottom element $\bot$, the bottom element is not in $s$ if and only if every element $x \in s$ is strictly greater than $\bot$, i.e., $\bot \notin s \leftrightarrow \forall x \in s, \bot < x$.

not_isMax_bot theorem

: ¬IsMax (⊥ : α)

Full source

theorem not_isMax_bot : ¬IsMax (⊥ : α) :=
  @not_isMin_top αᵒᵈ _ _ _

Bottom Element is Not Maximal in a Partially Ordered Set

Informal description

In a partially ordered set $\alpha$ with a least element $\bot$, the element $\bot$ is not a maximal element. That is, there does not exist an element $x \in \alpha$ such that $\bot \leq x$ and $x \neq \bot$.

OrderBot.ext_bot theorem

 {α} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α)
  (H :
    ∀ x y : α,
      (haveI := hA;
        x ≤ y) ↔
        x ≤ y) :
  (@Bot.bot α (@OrderBot.toBot α hA.toLE A)) = (@Bot.bot α (@OrderBot.toBot α hB.toLE B))

Full source

theorem OrderBot.ext_bot {α} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α}
    (B : OrderBot α) (H : ∀ x y : α, (haveI := hA; x ≤ y) ↔ x ≤ y) :
    (@Bot.bot α (@OrderBot.toBot α hA.toLE A)) = (@Bot.bot α (@OrderBot.toBot α hB.toLE B)) := by
  cases PartialOrder.ext H
  apply bot_unique
  exact @bot_le _ _ A _

Equality of Bottom Elements Under Equivalent Orderings

Informal description

Let $\alpha$ be a type with two partial orders $h_A$ and $h_B$, and let $A$ and $B$ be instances of `OrderBot` on $\alpha$ with respect to $h_A$ and $h_B$ respectively. If the two partial orders $h_A$ and $h_B$ induce the same ordering relation on $\alpha$ (i.e., for all $x, y \in \alpha$, $x \leq y$ under $h_A$ if and only if $x \leq y$ under $h_B$), then the bottom elements $\bot_A$ and $\bot_B$ defined by $A$ and $B$ are equal.

BoundedOrder structure

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

Full source

/-- A bounded order describes an order `(≤)` with a top and bottom element,
  denoted `⊤` and `⊥` respectively. -/
class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α

Bounded Order

Informal description

A bounded order is a partially ordered set equipped with both a greatest element (denoted $\top$) and a least element (denoted $\bot$). This structure extends both `OrderTop` (which provides $\top$) and `OrderBot` (which provides $\bot$).

OrderDual.instBoundedOrder instance

(α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ

Full source

instance OrderDual.instBoundedOrder (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ where
  __ := inferInstanceAs (OrderTop αᵒᵈ)
  __ := inferInstanceAs (OrderBot αᵒᵈ)

Bounded Order Duality

Informal description

For any type $\alpha$ with a partial order and both a greatest element $\top$ and a least element $\bot$, the order dual $\alpha^{\text{op}}$ also has a greatest element $\top$ and a least element $\bot$.

OrderBot.instSubsingleton instance

: Subsingleton (OrderBot α)

Full source

instance OrderBot.instSubsingleton : Subsingleton (OrderBot α) where
  allEq := by rintro @⟨⟨a⟩, ha⟩ @⟨⟨b⟩, hb⟩; congr; exact le_antisymm (ha _) (hb _)

Uniqueness of Order with Bottom Element

Informal description

For any type $\alpha$ with a partial order, there is at most one way to equip it with a bottom element $\bot$ that is less than or equal to all other elements.

OrderTop.instSubsingleton instance

: Subsingleton (OrderTop α)

Full source

instance OrderTop.instSubsingleton : Subsingleton (OrderTop α) where
  allEq := by rintro @⟨⟨a⟩, ha⟩ @⟨⟨b⟩, hb⟩; congr; exact le_antisymm (hb _) (ha _)

Uniqueness of Order with Top Element

Informal description

For any type $\alpha$ with a partial order, there is at most one way to equip it with a top element $\top$ that is greater than or equal to all other elements.

BoundedOrder.instSubsingleton instance

: Subsingleton (BoundedOrder α)

Full source

instance BoundedOrder.instSubsingleton : Subsingleton (BoundedOrder α) where
  allEq := by rintro ⟨⟩ ⟨⟩; congr <;> exact Subsingleton.elim _ _

Uniqueness of Bounded Order Structure

Informal description

For any type $\alpha$ with a partial order, there is at most one way to equip it with both a top element $\top$ and a bottom element $\bot$ that satisfy the bounded order properties.

Pi.instBotForall instance

[∀ i, Bot (α' i)] : Bot (∀ i, α' i)

Full source

instance [∀ i, Bot (α' i)] : Bot (∀ i, α' i) :=
  ⟨fun _ => ⊥⟩

Bottom Element in Product of Types with Bottom Elements

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ has a bottom element $\bot$, the product type $\forall i, \alpha_i$ also has a bottom element, defined pointwise as the function that returns $\bot$ for every index $i$.

Pi.bot_apply theorem

[∀ i, Bot (α' i)] (i : ι) : (⊥ : ∀ i, α' i) i = ⊥

Full source

@[simp]
theorem bot_apply [∀ i, Bot (α' i)] (i : ι) : (⊥ : ∀ i, α' i) i = ⊥ :=
  rfl

Pointwise Evaluation of Bottom Element in Product Type

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ has a bottom element $\bot$, and for any index $i \in \iota$, the evaluation of the bottom element of the product type $\forall i, \alpha_i$ at index $i$ equals $\bot$, i.e., $(\bot)_i = \bot$.

Pi.bot_def theorem

[∀ i, Bot (α' i)] : (⊥ : ∀ i, α' i) = fun _ => ⊥

Full source

theorem bot_def [∀ i, Bot (α' i)] : (⊥ : ∀ i, α' i) = fun _ => ⊥ :=
  rfl

Definition of Bottom Element in Product Type as Constant Function

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ has a bottom element $\bot$, the bottom element of the product type $\forall i, \alpha_i$ is the constant function that returns $\bot$ for every index $i$. In other words, $\bot = \lambda \_. \bot$.

Pi.instTopForall instance

[∀ i, Top (α' i)] : Top (∀ i, α' i)

Full source

instance [∀ i, Top (α' i)] : Top (∀ i, α' i) :=
  ⟨fun _ => ⊤⟩

Pointwise Top Element for Function Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ has a top element $\top$, the type of functions $\forall i, \alpha' i$ also has a top element, defined pointwise as the function that returns $\top$ for every input.

Pi.top_apply theorem

[∀ i, Top (α' i)] (i : ι) : (⊤ : ∀ i, α' i) i = ⊤

Full source

@[simp]
theorem top_apply [∀ i, Top (α' i)] (i : ι) : (⊤ : ∀ i, α' i) i = ⊤ :=
  rfl

Pointwise Evaluation of Top Function Yields Top Element

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ has a top element $\top$, the top element of the function type $\forall i, \alpha' i$ evaluated at any index $i$ equals $\top$. That is, $(\top : \forall i, \alpha' i)(i) = \top$.

Pi.top_def theorem

[∀ i, Top (α' i)] : (⊤ : ∀ i, α' i) = fun _ => ⊤

Full source

theorem top_def [∀ i, Top (α' i)] : (⊤ : ∀ i, α' i) = fun _ => ⊤ :=
  rfl

Top Element of Function Type is Constant Top Function

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ has a top element $\top$, the top element of the function type $\forall i, \alpha' i$ is the constant function that maps every input to $\top$.

Pi.instOrderTop instance

[∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i)

Full source

instance instOrderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) where
  le_top _ := fun _ => le_top

Pointwise Order and Top Element in Product of Ordered Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a partial order and has a greatest element $\top$, the product type $\forall i, \alpha_i$ is also equipped with a partial order and has a greatest element, defined pointwise as the function that returns $\top$ for every index $i$.

Pi.instOrderBot instance

[∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i)

Full source

instance instOrderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) where
  bot_le _ := fun _ => bot_le

Pointwise Order and Bottom Element in Product of Ordered Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a partial order and has a least element $\bot$, the product type $\forall i, \alpha_i$ is also equipped with a partial order and has a least element, defined pointwise as the function that returns $\bot$ for every index $i$.

Pi.instBoundedOrder instance

[∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] : BoundedOrder (∀ i, α' i)

Full source

instance instBoundedOrder [∀ i, LE (α' i)] [∀ i, BoundedOrder (α' i)] :
    BoundedOrder (∀ i, α' i) where
  __ := inferInstanceAs (OrderTop (∀ i, α' i))
  __ := inferInstanceAs (OrderBot (∀ i, α' i))

Pointwise Bounded Order in Product of Ordered Types

Informal description

For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a partial order and has both a greatest element $\top$ and a least element $\bot$, the product type $\forall i, \alpha_i$ is also equipped with a partial order and has both a greatest and least element, defined pointwise as the functions that return $\top$ and $\bot$ respectively for every index $i$.

subsingleton_of_top_le_bot theorem

(h : (⊤ : α) ≤ (⊥ : α)) : Subsingleton α

Full source

theorem subsingleton_of_top_le_bot (h : (⊤ : α) ≤ (⊥ : α)) : Subsingleton α :=
  ⟨fun _ _ => le_antisymm
    (le_trans le_top <| le_trans h bot_le) (le_trans le_top <| le_trans h bot_le)⟩

Subsingleton from $\top \leq \bot$

Informal description

If in an order $\alpha$ the top element $\top$ is less than or equal to the bottom element $\bot$, then $\alpha$ is a subsingleton (i.e., has at most one element).

subsingleton_of_bot_eq_top theorem

(hα : (⊥ : α) = (⊤ : α)) : Subsingleton α

Full source

theorem subsingleton_of_bot_eq_top (hα : (⊥ : α) = (⊤ : α)) : Subsingleton α :=
  subsingleton_of_top_le_bot (ge_of_eq hα)

Subsingleton from $\bot = \top$

Informal description

If in an order $\alpha$ the bottom element $\bot$ is equal to the top element $\top$, then $\alpha$ is a subsingleton (i.e., has at most one element).

subsingleton_iff_bot_eq_top theorem

: (⊥ : α) = (⊤ : α) ↔ Subsingleton α

Full source

theorem subsingleton_iff_bot_eq_top : (⊥ : α) = (⊤ : α) ↔ Subsingleton α :=
  ⟨subsingleton_of_bot_eq_top, fun _ => Subsingleton.elim ⊥ ⊤⟩

$\bot = \top$ iff Order is Subsingleton

Informal description

For any type $\alpha$ with a partial order and both top ($\top$) and bottom ($\bot$) elements, the equality $\bot = \top$ holds if and only if $\alpha$ is a subsingleton (i.e., has at most one element).

OrderTop.lift abbrev

 [LE α] [Top α] [LE β] [OrderTop β] (f : α → β) (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) : OrderTop α

Full source

/-- Pullback an `OrderTop`. -/
abbrev OrderTop.lift [LE α] [Top α] [LE β] [OrderTop β] (f : α → β)
    (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) : OrderTop α :=
  ⟨fun a =>
    map_le _ _ <| by
      rw [map_top]
      exact le_top _⟩

Lifting an Order with Top Element via a Reflecting Function

Informal description

Let $\alpha$ and $\beta$ be partially ordered types, where $\beta$ has a greatest element $\top_\beta$ (i.e., $\beta$ is an `OrderTop`). Given a function $f : \alpha \to \beta$ that satisfies: 1. For any $a, b \in \alpha$, if $f(a) \leq f(b)$ then $a \leq b$ (i.e., $f$ reflects the order), 2. $f(\top_\alpha) = \top_\beta$ (where $\top_\alpha$ is the top element of $\alpha$ and $\top_\beta$ is the top element of $\beta$), then $\alpha$ inherits an `OrderTop` structure from $\beta$ via $f$.

OrderBot.lift abbrev

 [LE α] [Bot α] [LE β] [OrderBot β] (f : α → β) (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_bot : f ⊥ = ⊥) : OrderBot α

Full source

/-- Pullback an `OrderBot`. -/
abbrev OrderBot.lift [LE α] [Bot α] [LE β] [OrderBot β] (f : α → β)
    (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_bot : f ⊥ = ⊥) : OrderBot α :=
  ⟨fun a =>
    map_le _ _ <| by
      rw [map_bot]
      exact bot_le _⟩

Lifting an Order with Bottom Element via a Reflecting Function

Informal description

Let $\alpha$ and $\beta$ be types with a partial order $\leq$, where $\beta$ has a least element $\bot$ (i.e., $\beta$ is an `OrderBot`). Given a function $f : \alpha \to \beta$ that satisfies: 1. For any $a, b \in \alpha$, if $f(a) \leq f(b)$ then $a \leq b$ (i.e., $f$ reflects the order), 2. $f(\bot_\alpha) = \bot_\beta$ (where $\bot_\alpha$ is the bottom element of $\alpha$ and $\bot_\beta$ is the bottom element of $\beta$), then $\alpha$ inherits an `OrderBot` structure from $\beta$ via $f$.

BoundedOrder.lift abbrev

 [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β) (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) : BoundedOrder α

Full source

/-- Pullback a `BoundedOrder`. -/
abbrev BoundedOrder.lift [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β)
    (map_le : ∀ a b, f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :
    BoundedOrder α where
  __ := OrderTop.lift f map_le map_top
  __ := OrderBot.lift f map_le map_bot

Lifting a Bounded Order via a Reflecting Function

Informal description

Let $\alpha$ and $\beta$ be partially ordered types, where $\beta$ has both a greatest element $\top$ and a least element $\bot$ (i.e., $\beta$ is a `BoundedOrder`). Given a function $f : \alpha \to \beta$ that satisfies: 1. For any $a, b \in \alpha$, if $f(a) \leq f(b)$ then $a \leq b$ (i.e., $f$ reflects the order), 2. $f(\top_\alpha) = \top_\beta$ (where $\top_\alpha$ is the top element of $\alpha$ and $\top_\beta$ is the top element of $\beta$), 3. $f(\bot_\alpha) = \bot_\beta$ (where $\bot_\alpha$ is the bottom element of $\alpha$ and $\bot_\beta$ is the bottom element of $\beta$), then $\alpha$ inherits a `BoundedOrder` structure from $\beta$ via $f$.

Subtype.orderBot abbrev

[LE α] [OrderBot α] (hbot : p ⊥) : OrderBot { x : α // p x }

Full source

/-- A subtype remains a `⊥`-order if the property holds at `⊥`. -/
protected abbrev orderBot [LE α] [OrderBot α] (hbot : p ⊥) : OrderBot { x : α // p x } where
  bot := ⟨⊥, hbot⟩
  bot_le _ := bot_le

Subtype Inherits Bottom Element When Predicate Holds at Bottom

Informal description

Let $\alpha$ be a type with a partial order $\leq$ and a least element $\bot$ (i.e., $\alpha$ is an `OrderBot`). Given a predicate $p$ on $\alpha$ such that $p(\bot)$ holds, then the subtype $\{x \in \alpha \mid p(x)\}$ inherits an `OrderBot` structure from $\alpha$, with $\bot$ as its least element.

Subtype.orderTop abbrev

[LE α] [OrderTop α] (htop : p ⊤) : OrderTop { x : α // p x }

Full source

/-- A subtype remains a `⊤`-order if the property holds at `⊤`. -/
protected abbrev orderTop [LE α] [OrderTop α] (htop : p ⊤) : OrderTop { x : α // p x } where
  top := ⟨⊤, htop⟩
  le_top _ := le_top

Subtype Inherits Top Element When Predicate Holds at Top

Informal description

Let $\alpha$ be a type with a partial order $\leq$ and a greatest element $\top$ (i.e., $\alpha$ is an `OrderTop`). Given a predicate $p$ on $\alpha$ such that $p(\top)$ holds, then the subtype $\{x \in \alpha \mid p(x)\}$ inherits an `OrderTop` structure from $\alpha$, with $\top$ as its greatest element.

Subtype.boundedOrder abbrev

[LE α] [BoundedOrder α] (hbot : p ⊥) (htop : p ⊤) : BoundedOrder (Subtype p)

Full source

/-- A subtype remains a bounded order if the property holds at `⊥` and `⊤`. -/
protected abbrev boundedOrder [LE α] [BoundedOrder α] (hbot : p ⊥) (htop : p ⊤) :
    BoundedOrder (Subtype p) where
  __ := Subtype.orderTop htop
  __ := Subtype.orderBot hbot

Subtype Inherits Bounded Order When Predicate Holds at Top and Bottom

Informal description

Let $\alpha$ be a type with a partial order $\leq$ and both a greatest element $\top$ and a least element $\bot$ (i.e., $\alpha$ is a `BoundedOrder`). Given a predicate $p$ on $\alpha$ such that $p(\bot)$ and $p(\top)$ hold, then the subtype $\{x \in \alpha \mid p(x)\}$ inherits a `BoundedOrder` structure from $\alpha$, with $\bot$ and $\top$ as its least and greatest elements, respectively.

Subtype.mk_bot theorem

[OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) : mk ⊥ hbot = ⊥

Full source

@[simp]
theorem mk_bot [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) : mk ⊥ hbot = ⊥ :=
  le_bot_iff.1 <| coe_le_coe.1 bot_le

Subtype Bottom Element Construction via Predicate

Informal description

Let $\alpha$ be a type with a least element $\bot$ (i.e., $\alpha$ is an `OrderBot`), and let $p$ be a predicate on $\alpha$ such that $p(\bot)$ holds. Then, the bottom element of the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the term constructed by applying the subtype constructor `mk` to $\bot$ and the proof $hbot$ that $p(\bot)$ holds.

Subtype.mk_top theorem

[OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) : mk ⊤ htop = ⊤

Full source

@[simp]
theorem mk_top [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) : mk ⊤ htop = ⊤ :=
  top_le_iff.1 <| coe_le_coe.1 le_top

Subtype Greatest Element Construction Preserves Top

Informal description

Let $\alpha$ be a type with an order and a greatest element $\top$ (i.e., an `OrderTop`), and let $p$ be a predicate on $\alpha$ such that $p(\top)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderTop` structure, then the element $\top$ in the subtype (constructed as `mk ⊤ htop`) is equal to the greatest element $\top$ of the subtype.

Subtype.coe_bot theorem

[OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) : ((⊥ : Subtype p) : α) = ⊥

Full source

theorem coe_bot [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) : ((⊥ : Subtype p) : α) = ⊥ :=
  congr_arg Subtype.val (mk_bot hbot).symm

Coercion of Subtype Bottom Element Equals Parent Bottom Element

Informal description

Let $\alpha$ be a type with a least element $\bot$ (i.e., $\alpha$ is an `OrderBot`), and let $p$ be a predicate on $\alpha$ such that $p(\bot)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderBot` structure, then the coercion of the bottom element $\bot$ of the subtype to $\alpha$ is equal to the bottom element $\bot$ of $\alpha$.

Subtype.coe_top theorem

[OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) : ((⊤ : Subtype p) : α) = ⊤

Full source

theorem coe_top [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) : ((⊤ : Subtype p) : α) = ⊤ :=
  congr_arg Subtype.val (mk_top htop).symm

Coercion of Subtype's Top Element to Original Type Equals Top Element

Informal description

Let $\alpha$ be a type with an order and a greatest element $\top$ (i.e., an `OrderTop`), and let $p$ be a predicate on $\alpha$ such that $p(\top)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderTop` structure, then the coercion of the greatest element $\top$ of the subtype to $\alpha$ is equal to the greatest element $\top$ of $\alpha$.

Subtype.coe_eq_bot_iff theorem

[OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : { x // p x }} : (x : α) = ⊥ ↔ x = ⊥

Full source

@[simp]
theorem coe_eq_bot_iff [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : { x // p x }} :
    (x : α) = ⊥ ↔ x = ⊥ := by
  rw [← coe_bot hbot, Subtype.ext_iff]

Equivalence of Coercion to Bottom and Subtype Bottom Element

Informal description

Let $\alpha$ be a type with a least element $\bot$ (i.e., $\alpha$ is an `OrderBot`), and let $p$ be a predicate on $\alpha$ such that $p(\bot)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderBot` structure, then for any element $x$ in the subtype, the coercion of $x$ to $\alpha$ equals $\bot$ if and only if $x$ is the bottom element of the subtype.

Subtype.coe_eq_top_iff theorem

[OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : { x // p x }} : (x : α) = ⊤ ↔ x = ⊤

Full source

@[simp]
theorem coe_eq_top_iff [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : { x // p x }} :
    (x : α) = ⊤ ↔ x = ⊤ := by
  rw [← coe_top htop, Subtype.ext_iff]

Equivalence of Coercion to Top and Subtype Top Element

Informal description

Let $\alpha$ be a type with an order and a greatest element $\top$ (i.e., an `OrderTop`), and let $p$ be a predicate on $\alpha$ such that $p(\top)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderTop` structure, then for any element $x$ in the subtype, the coercion of $x$ to $\alpha$ equals $\top$ if and only if $x$ is the greatest element $\top$ of the subtype.

Subtype.mk_eq_bot_iff theorem

[OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : α} (hx : p x) : (⟨x, hx⟩ : Subtype p) = ⊥ ↔ x = ⊥

Full source

@[simp]
theorem mk_eq_bot_iff [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : α} (hx : p x) :
    (⟨x, hx⟩ : Subtype p) = ⊥ ↔ x = ⊥ :=
  (coe_eq_bot_iff hbot).symm

Equivalence of Subtype Construction with Bottom and Bottom Element in Base Type

Informal description

Let $\alpha$ be a type with a least element $\bot$ (i.e., $\alpha$ is an `OrderBot`), and let $p$ be a predicate on $\alpha$ such that $p(\bot)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderBot` structure, then for any element $x \in \alpha$ satisfying $p(x)$, the element $\langle x, hx \rangle$ of the subtype is equal to $\bot$ if and only if $x = \bot$.

Subtype.mk_eq_top_iff theorem

[OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : α} (hx : p x) : (⟨x, hx⟩ : Subtype p) = ⊤ ↔ x = ⊤

Full source

@[simp]
theorem mk_eq_top_iff [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : α} (hx : p x) :
    (⟨x, hx⟩ : Subtype p) = ⊤ ↔ x = ⊤ :=
  (coe_eq_top_iff htop).symm

Equivalence of Subtype Top Element and Coercion to Top in Base Type

Informal description

Let $\alpha$ be a type with an order and a greatest element $\top$ (i.e., an `OrderTop`), and let $p$ be a predicate on $\alpha$ such that $p(\top)$ holds. If the subtype $\{x \in \alpha \mid p(x)\}$ also has an `OrderTop` structure, then for any element $x \in \alpha$ satisfying $p(x)$, the element $\langle x, hx \rangle$ in the subtype is equal to the greatest element $\top$ of the subtype if and only if $x = \top$ in $\alpha$.

Prod.instTop instance

[Top α] [Top β] : Top (α × β)

Full source

instance instTop [Top α] [Top β] : Top (α × β) :=
  ⟨⟨⊤, ⊤⟩⟩

Top Element in Product Type

Informal description

For any types $α$ and $β$ with top elements, the product type $α × β$ also has a top element.

Prod.instBot instance

[Bot α] [Bot β] : Bot (α × β)

Full source

instance instBot [Bot α] [Bot β] : Bot (α × β) :=
  ⟨⟨⊥, ⊥⟩⟩

Bottom Element in Product Type

Informal description

For types $\alpha$ and $\beta$ each equipped with a bottom element $\bot$, the product type $\alpha \times \beta$ is also equipped with a bottom element, defined componentwise as $(\bot, \bot)$.

Prod.fst_top theorem

[Top α] [Top β] : (⊤ : α × β).fst = ⊤

Full source

@[simp] lemma fst_top [Top α] [Top β] : (⊤ : α × β).fst = ⊤ := rfl

First Projection of Top Element in Product Type

Informal description

For any types $\alpha$ and $\beta$ with top elements $\top_\alpha$ and $\top_\beta$ respectively, the first projection of the top element in the product type $\alpha \times \beta$ equals the top element of $\alpha$, i.e., $(\top_{\alpha \times \beta}).\mathrm{fst} = \top_\alpha$.

Prod.snd_top theorem

[Top α] [Top β] : (⊤ : α × β).snd = ⊤

Full source

@[simp] lemma snd_top [Top α] [Top β] : (⊤ : α × β).snd = ⊤ := rfl

Second Component of Top Element in Product Type Equals Top

Informal description

For any types $\alpha$ and $\beta$ with top elements $\top$, the second component of the top element in the product type $\alpha \times \beta$ is equal to the top element of $\beta$, i.e., $(\top : \alpha \times \beta).\mathrm{snd} = \top$.

Prod.fst_bot theorem

[Bot α] [Bot β] : (⊥ : α × β).fst = ⊥

Full source

@[simp] lemma fst_bot [Bot α] [Bot β] : (⊥ : α × β).fst = ⊥ := rfl

First Projection of Bottom Element in Product Type

Informal description

For types $\alpha$ and $\beta$ each equipped with a bottom element $\bot$, the first projection of the bottom element in the product type $\alpha \times \beta$ equals the bottom element of $\alpha$, i.e., $(\bot : \alpha \times \beta).\mathrm{fst} = \bot$.

Prod.snd_bot theorem

[Bot α] [Bot β] : (⊥ : α × β).snd = ⊥

Full source

@[simp] lemma snd_bot [Bot α] [Bot β] : (⊥ : α × β).snd = ⊥ := rfl

Second Projection of Bottom in Product Type Equals Bottom

Informal description

For types $\alpha$ and $\beta$ each equipped with a bottom element $\bot$, the second projection of the bottom element in the product type $\alpha \times \beta$ equals the bottom element of $\beta$, i.e., $(\bot : \alpha \times \beta).\text{snd} = \bot$.

Prod.instOrderTop instance

[LE α] [LE β] [OrderTop α] [OrderTop β] : OrderTop (α × β)

Full source

instance instOrderTop [LE α] [LE β] [OrderTop α] [OrderTop β] : OrderTop (α × β) where
  __ := inferInstanceAs (Top (α × β))
  le_top _ := ⟨le_top, le_top⟩

Order Top Structure on Product Types

Informal description

For any types $\alpha$ and $\beta$ with order top structures (i.e., each has a greatest element $\top$ and a partial order $\leq$), the product type $\alpha \times \beta$ inherits an order top structure where the greatest element is $(\top, \top)$ and the order is defined componentwise.

Prod.instOrderBot instance

[LE α] [LE β] [OrderBot α] [OrderBot β] : OrderBot (α × β)

Full source

instance instOrderBot [LE α] [LE β] [OrderBot α] [OrderBot β] : OrderBot (α × β) where
  __ := inferInstanceAs (Bot (α × β))
  bot_le _ := ⟨bot_le, bot_le⟩

Order Bot Structure on Product Types

Informal description

For any types $\alpha$ and $\beta$ with order bot structures (i.e., each has a least element $\bot$ and a partial order $\leq$), the product type $\alpha \times \beta$ inherits an order bot structure where the least element is $(\bot, \bot)$ and the order is defined componentwise.

Prod.instBoundedOrder instance

[LE α] [LE β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (α × β)

Full source

instance instBoundedOrder [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] :
    BoundedOrder (α × β) where
  __ := inferInstanceAs (OrderTop (α × β))
  __ := inferInstanceAs (OrderBot (α × β))

Bounded Order Structure on Product Types

Informal description

For any types $\alpha$ and $\beta$ with bounded order structures (i.e., each has both a greatest element $\top$ and a least element $\bot$ with respect to their partial orders), the product type $\alpha \times \beta$ inherits a bounded order structure where the greatest element is $(\top, \top)$, the least element is $(\bot, \bot)$, and the order is defined componentwise.

ULift.instTop instance

[Top α] : Top (ULift.{v} α)

Full source

instance [Top α] : Top (ULift.{v} α) where top := up ⊤

Top Element in Lifted Type

Informal description

For any type $\alpha$ with a top element $\top$, the lifted type $\text{ULift}\, \alpha$ also has a top element.

ULift.up_top theorem

[Top α] : up (⊤ : α) = ⊤

Full source

@[simp] theorem up_top [Top α] : up (⊤ : α) = ⊤ := rfl

Lifting Preserves Top Element: $\text{up}(\top) = \top$

Informal description

For any type $\alpha$ with a top element $\top$, the lifting of $\top$ via the `up` function equals the top element in the lifted type $\text{ULift}\, \alpha$, i.e., $\text{up}(\top) = \top$.

ULift.down_top theorem

[Top α] : down (⊤ : ULift α) = ⊤

Full source

@[simp] theorem down_top [Top α] : down (⊤ : ULift α) = ⊤ := rfl

Projection of Top Element in Lifted Type Equals Original Top Element

Informal description

For any type $\alpha$ with a top element $\top$, the projection of the top element from the lifted type $\text{ULift}\, \alpha$ back to $\alpha$ equals $\top$, i.e., $\text{down}(\top : \text{ULift}\, \alpha) = \top$.

ULift.instBot instance

[Bot α] : Bot (ULift.{v} α)

Full source

instance [Bot α] : Bot (ULift.{v} α) where bot := up ⊥

Bottom Element in Lifted Type

Informal description

For any type $\alpha$ with a bottom element $\bot$, the lifted type $\text{ULift}\, \alpha$ also has a bottom element.

ULift.up_bot theorem

[Bot α] : up (⊥ : α) = ⊥

Full source

@[simp] theorem up_bot [Bot α] : up (⊥ : α) = ⊥ := rfl

Lifting Preserves Bottom Element: $\text{up}(\bot) = \bot$

Informal description

For any type $\alpha$ with a bottom element $\bot$, the lifting function $\text{up}$ maps $\bot$ in $\alpha$ to $\bot$ in the lifted type $\text{ULift}\, \alpha$, i.e., $\text{up}(\bot) = \bot$.

ULift.down_bot theorem

[Bot α] : down (⊥ : ULift α) = ⊥

Full source

@[simp] theorem down_bot [Bot α] : down (⊥ : ULift α) = ⊥ := rfl

Unlifting Preserves Bottom Element: $\text{down}(\bot) = \bot$

Informal description

For any type $\alpha$ with a bottom element $\bot$, the unlifting function $\text{down}$ maps $\bot$ in the lifted type $\text{ULift}\, \alpha$ to $\bot$ in $\alpha$, i.e., $\text{down}(\bot) = \bot$.

ULift.instOrderBot instance

[LE α] [OrderBot α] : OrderBot (ULift.{v} α)

Full source

instance [LE α] [OrderBot α] : OrderBot (ULift.{v} α) :=
  OrderBot.lift ULift.down (fun _ _ => down_le.mp) down_bot

Lifted Type Inherits Order with Bottom Element

Informal description

For any partially ordered type $\alpha$ with a least element $\bot$, the lifted type $\text{ULift}\, \alpha$ also has a least element with respect to the inherited order.

ULift.instOrderTop instance

[LE α] [OrderTop α] : OrderTop (ULift.{v} α)

Full source

instance [LE α] [OrderTop α] : OrderTop (ULift.{v} α) :=
  OrderTop.lift ULift.down (fun _ _ => down_le.mp) down_top

Lifted Type Inherits Order with Top Element

Informal description

For any partially ordered type $\alpha$ with a greatest element $\top$, the lifted type $\text{ULift}\, \alpha$ also has a greatest element with respect to the inherited order.

ULift.instBoundedOrder instance

[LE α] [BoundedOrder α] : BoundedOrder (ULift.{v} α)

Full source

instance [LE α] [BoundedOrder α] : BoundedOrder (ULift.{v} α) where

Lifted Type Inherits Bounded Order Structure

Informal description

For any partially ordered type $\alpha$ with both a greatest element $\top$ and a least element $\bot$, the lifted type $\text{ULift}\, \alpha$ also has both a greatest and a least element with respect to the inherited order.

bot_ne_top theorem

: (⊥ : α) ≠ ⊤

Full source

@[simp]
theorem bot_ne_top : (⊥ : α) ≠ ⊤ := fun h => not_subsingleton _ <| subsingleton_of_bot_eq_top h

Bottom and Top Elements are Distinct in a Bounded Order

Informal description

In a bounded order $\alpha$, the bottom element $\bot$ is not equal to the top element $\top$, i.e., $\bot \neq \top$.

top_ne_bot theorem

: (⊤ : α) ≠ ⊥

Full source

@[simp]
theorem top_ne_bot : (⊤ : α) ≠ ⊥ :=
  bot_ne_top.symm

Top and Bottom Elements are Distinct in a Bounded Order

Informal description

In a bounded order $\alpha$, the top element $\top$ is not equal to the bottom element $\bot$, i.e., $\top \neq \bot$.

bot_lt_top theorem

: (⊥ : α) < ⊤

Full source

@[simp]
theorem bot_lt_top : (⊥ : α) < ⊤ :=
  lt_top_iff_ne_top.2 bot_ne_top

Bottom Element is Strictly Less Than Top Element in Bounded Order

Informal description

In a bounded order $\alpha$, the bottom element $\bot$ is strictly less than the top element $\top$, i.e., $\bot < \top$.

Bool.instBoundedOrder instance

: BoundedOrder Bool

Full source

instance Bool.instBoundedOrder : BoundedOrder Bool where
  top := true
  le_top := Bool.le_true
  bot := false
  bot_le := Bool.false_le

Bounded Order Structure on Boolean Values

Informal description

The Boolean type `Bool` is a bounded order, where `true` is the greatest element (⊤) and `false` is the least element (⊥).

top_eq_true theorem

: ⊤ = true

Full source

@[simp]
theorem top_eq_true : ⊤ = true :=
  rfl

Top Element in Boolean Type is True

Informal description

In the Boolean type, the top element $\top$ is equal to `true`.

bot_eq_false theorem

: ⊥ = false

Full source

@[simp]
theorem bot_eq_false : ⊥ = false :=
  rfl

Bottom Element in Boolean Type is False

Informal description

In the Boolean type, the bottom element $\bot$ is equal to `false`.

Main declarations