Mathlib.Order.WithBot

WithBot.nontrivial instance

[Nonempty α] : Nontrivial (WithBot α)

Full source

instance nontrivial [Nonempty α] : Nontrivial (WithBot α) :=
  Option.nontrivial

Nontriviality of $\text{WithBot}\,\alpha$ for Nonempty $\alpha$

Informal description

For any nonempty type $\alpha$, the type $\text{WithBot}\,\alpha$ (obtained by adjoining a bottom element to $\alpha$) is nontrivial, meaning it contains at least two distinct elements.

WithBot.coe_injective theorem

: Injective ((↑) : α → WithBot α)

Full source

theorem coe_injective : Injective ((↑) : α → WithBot α) :=
  Option.some_injective _

Injectivity of the Embedding from $\alpha$ to $\text{WithBot}\,\alpha$

Informal description

The canonical embedding function from a type $\alpha$ to $\text{WithBot}\,\alpha$ is injective. That is, for any $x, y \in \alpha$, if $x = y$ in $\text{WithBot}\,\alpha$, then $x = y$ in $\alpha$.

WithBot.coe_inj theorem

: (a : WithBot α) = b ↔ a = b

Full source

@[simp, norm_cast]
theorem coe_inj : (a : WithBot α) = b ↔ a = b :=
  Option.some_inj

Injectivity of the Embedding from $\alpha$ to $\text{WithBot}\,\alpha$

Informal description

For any elements $a, b \in \alpha$, the canonical embeddings of $a$ and $b$ into $\text{WithBot}\,\alpha$ are equal if and only if $a = b$ in $\alpha$.

WithBot.forall theorem

{p : WithBot α → Prop} : (∀ x, p x) ↔ p ⊥ ∧ ∀ x : α, p x

Full source

protected theorem «forall» {p : WithBot α → Prop} : (∀ x, p x) ↔ p ⊥ ∧ ∀ x : α, p x :=
  Option.forall

Universal Quantification over $\text{WithBot}\,\alpha$: Bottom and All in $\alpha$

Informal description

For any predicate $p$ on $\text{WithBot}\,\alpha$, the statement $(\forall x \in \text{WithBot}\,\alpha, p(x))$ holds if and only if $p(\bot)$ holds and for all $x \in \alpha$, $p(x)$ holds.

WithBot.exists theorem

{p : WithBot α → Prop} : (∃ x, p x) ↔ p ⊥ ∨ ∃ x : α, p x

Full source

protected theorem «exists» {p : WithBot α → Prop} : (∃ x, p x) ↔ p ⊥ ∨ ∃ x : α, p x :=
  Option.exists

Existence in $\text{WithBot}\,\alpha$: Bottom or Lift from $\alpha$

Informal description

For any predicate $p$ on $\text{WithBot}\,\alpha$, there exists an element $x$ in $\text{WithBot}\,\alpha$ satisfying $p(x)$ if and only if either $p(\bot)$ holds or there exists an element $x$ in $\alpha$ such that $p(x)$ holds.

WithBot.none_eq_bot theorem

: (none : WithBot α) = (⊥ : WithBot α)

Full source

theorem none_eq_bot : (none : WithBot α) = (⊥ : WithBot α) :=
  rfl

Equality of `none` and Bottom in `WithBot α`

Informal description

In the type `WithBot α`, the element `none` is equal to the bottom element `⊥`.

WithBot.some_eq_coe theorem

(a : α) : (Option.some a : WithBot α) = (↑a : WithBot α)

Full source

theorem some_eq_coe (a : α) : (Option.some a : WithBot α) = (↑a : WithBot α) :=
  rfl

Equality of Embeddings in `WithBot α`

Informal description

For any element $a$ of type $\alpha$, the embedding of $a$ into `WithBot α` via `Option.some` is equal to the canonical embedding of $a$ into `WithBot α$.

WithBot.bot_ne_coe theorem

: ⊥ ≠ (a : WithBot α)

Full source

@[simp]
theorem bot_ne_coe : ⊥⊥ ≠ (a : WithBot α) :=
  nofun

Bottom element is distinct from any embedded element in `WithBot α`

Informal description

For any element $a$ of type $\alpha$, the bottom element $\bot$ in `WithBot α` is not equal to the embedding of $a$ into `WithBot α$.

WithBot.coe_ne_bot theorem

: (a : WithBot α) ≠ ⊥

Full source

@[simp]
theorem coe_ne_bot : (a : WithBot α) ≠ ⊥ :=
  nofun

Embedded elements are distinct from bottom in `WithBot α`

Informal description

For any element $a$ of type $\alpha$, the canonical embedding of $a$ into `WithBot α` is not equal to the bottom element $\bot$.

WithBot.unbotD definition

(d : α) (x : WithBot α) : α

Full source

/-- Specialization of `Option.getD` to values in `WithBot α` that respects API boundaries.
-/
def unbotD (d : α) (x : WithBot α) : α :=
  recBotCoe d id x

Default value extraction for `WithBot α`

Informal description

Given a default value $d$ of type $\alpha$ and an element $x$ of type `WithBot α`, the function returns $d$ if $x$ is the bottom element $\bot$, and returns the embedded value of $x$ otherwise.

WithBot.unbotD_bot theorem

{α} (d : α) : unbotD d ⊥ = d

Full source

@[simp]
theorem unbotD_bot {α} (d : α) : unbotD d ⊥ = d :=
  rfl

Default Extraction of Bottom Element in `WithBot`

Informal description

For any type $\alpha$ and element $d \in \alpha$, the function `unbotD` satisfies $\text{unbotD}\,d\,\bot = d$.

WithBot.unbotD_coe theorem

{α} (d x : α) : unbotD d x = x

Full source

@[simp]
theorem unbotD_coe {α} (d x : α) : unbotD d x = x :=
  rfl

Default Extraction Preserves Embedded Elements in `WithBot`

Informal description

For any type $\alpha$ and elements $d, x \in \alpha$, the function `unbotD` satisfies $\text{unbotD}\,d\,x = x$.

WithBot.coe_eq_coe theorem

: (a : WithBot α) = b ↔ a = b

Full source

theorem coe_eq_coe : (a : WithBot α) = b ↔ a = b := coe_inj

Equality of Embeddings in $\text{WithBot}\,\alpha$

Informal description

For any elements $a, b \in \alpha$, the canonical embeddings of $a$ and $b$ into $\text{WithBot}\,\alpha$ are equal if and only if $a = b$ in $\alpha$.

WithBot.unbotD_eq_iff theorem

{d y : α} {x : WithBot α} : unbotD d x = y ↔ x = y ∨ x = ⊥ ∧ y = d

Full source

theorem unbotD_eq_iff {d y : α} {x : WithBot α} : unbotDunbotD d x = y ↔ x = y ∨ x = ⊥ ∧ y = d := by
  induction x <;> simp [@eq_comm _ d]

Characterization of Equality for Default Value Extraction in $\text{WithBot}\,\alpha$

Informal description

For any default value $d$ and element $y$ in $\alpha$, and for any element $x$ in $\text{WithBot}\,\alpha$, the equality $\text{unbotD}\,d\,x = y$ holds if and only if either $x$ is equal to $y$ (as embedded elements), or $x$ is the bottom element $\bot$ and $y$ equals the default value $d$.

WithBot.unbotD_eq_self_iff theorem

{d : α} {x : WithBot α} : unbotD d x = d ↔ x = d ∨ x = ⊥

Full source

@[simp]
theorem unbotD_eq_self_iff {d : α} {x : WithBot α} : unbotDunbotD d x = d ↔ x = d ∨ x = ⊥ := by
  simp [unbotD_eq_iff]

Characterization of Default Value Extraction in $\text{WithBot}\,\alpha$

Informal description

For any default value $d$ in $\alpha$ and any element $x$ in $\text{WithBot}\,\alpha$, the equality $\text{unbotD}\,d\,x = d$ holds if and only if either $x$ is equal to $d$ (as an embedded element) or $x$ is the bottom element $\bot$.

WithBot.unbotD_eq_unbotD_iff theorem

{d : α} {x y : WithBot α} : unbotD d x = unbotD d y ↔ x = y ∨ x = d ∧ y = ⊥ ∨ x = ⊥ ∧ y = d

Full source

theorem unbotD_eq_unbotD_iff {d : α} {x y : WithBot α} :
    unbotDunbotD d x = unbotD d y ↔ x = y ∨ x = d ∧ y = ⊥ ∨ x = ⊥ ∧ y = d := by
  induction y <;> simp [unbotD_eq_iff, or_comm]

Equality Condition for Default Value Extraction in $\text{WithBot}\,\alpha$

Informal description

For any default value $d$ in $\alpha$ and elements $x, y$ in $\text{WithBot}\,\alpha$, the equality $\text{unbotD}\,d\,x = \text{unbotD}\,d\,y$ holds if and only if either $x = y$, or $x = d$ and $y = \bot$, or $x = \bot$ and $y = d$.

WithBot.map definition

(f : α → β) : WithBot α → WithBot β

Full source

/-- Lift a map `f : α → β` to `WithBot α → WithBot β`. Implemented using `Option.map`. -/
def map (f : α → β) : WithBot α → WithBot β :=
  Option.map f

Lifting a function to `WithBot`

Informal description

Given a function $f : \alpha \to \beta$, this function lifts $f$ to a function $\text{WithBot} \alpha \to \text{WithBot} \beta$ by applying $f$ to the values in $\alpha$ and mapping the bottom element $\bot$ to itself. This is implemented using the `Option.map` function.

WithBot.map_bot theorem

(f : α → β) : map f ⊥ = ⊥

Full source

@[simp]
theorem map_bot (f : α → β) : map f ⊥ = ⊥ :=
  rfl

Bottom Element Preservation under Mapping in `WithBot`

Informal description

For any function $f : \alpha \to \beta$, the lifted function $\text{map}\, f$ on $\text{WithBot}\, \alpha$ maps the bottom element $\bot$ to the bottom element $\bot$ in $\text{WithBot}\, \beta$, i.e., $\text{map}\, f\, \bot = \bot$.

WithBot.map_coe theorem

(f : α → β) (a : α) : map f a = f a

Full source

@[simp]
theorem map_coe (f : α → β) (a : α) : map f a = f a :=
  rfl

Lifted Function Evaluation on Embedded Elements in `WithBot`

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the lifted function $\text{map}\, f$ on $\text{WithBot}\, \alpha$ maps the element $a$ (embedded in $\text{WithBot}\, \alpha$) to $f(a)$ (embedded in $\text{WithBot}\, \beta$), i.e., $\text{map}\, f\, a = f(a)$.

WithBot.map_eq_bot_iff theorem

{f : α → β} {a : WithBot α} : map f a = ⊥ ↔ a = ⊥

Full source

@[simp]
lemma map_eq_bot_iff {f : α → β} {a : WithBot α} :
    mapmap f a = ⊥ ↔ a = ⊥ := Option.map_eq_none_iff

Characterization of Bottom Element Preservation under Mapping in `WithBot`

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \text{WithBot}\, \alpha$, the lifted function $\text{map}\, f$ maps $a$ to the bottom element $\bot$ in $\text{WithBot}\, \beta$ if and only if $a$ is the bottom element $\bot$ in $\text{WithBot}\, \alpha$. In other words, $\text{map}\, f\, a = \bot \leftrightarrow a = \bot$.

WithBot.map_eq_some_iff theorem

{f : α → β} {y : β} {v : WithBot α} : WithBot.map f v = .some y ↔ ∃ x, v = .some x ∧ f x = y

Full source

theorem map_eq_some_iff {f : α → β} {y : β} {v : WithBot α} :
    WithBot.mapWithBot.map f v = .some y ↔ ∃ x, v = .some x ∧ f x = y := Option.map_eq_some_iff

Characterization of `map` Output as `some` in `WithBot`

Informal description

For any function $f : \alpha \to \beta$, element $y \in \beta$, and element $v \in \text{WithBot} \alpha$, the following equivalence holds: $\text{map}\, f\, v = \text{some}\, y$ if and only if there exists $x \in \alpha$ such that $v = \text{some}\, x$ and $f(x) = y$.

WithBot.some_eq_map_iff theorem

{f : α → β} {y : β} {v : WithBot α} : .some y = WithBot.map f v ↔ ∃ x, v = .some x ∧ f x = y

Full source

theorem some_eq_map_iff {f : α → β} {y : β} {v : WithBot α} :
    .some.some y = WithBot.map f v ↔ ∃ x, v = .some x ∧ f x = y := by
  cases v <;> simp [eq_comm]

Characterization of `some` Equality under Mapping in `WithBot`

Informal description

For any function $f : \alpha \to \beta$, element $y \in \beta$, and element $v \in \text{WithBot}\, \alpha$, the following equivalence holds: $\text{some}\, y = \text{map}\, f\, v$ if and only if there exists $x \in \alpha$ such that $v = \text{some}\, x$ and $f(x) = y$.

WithBot.map_comm theorem

 {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
  map g₁ (map f₁ a) = map g₂ (map f₂ a)

Full source

theorem map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ}
    (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
    map g₁ (map f₁ a) = map g₂ (map f₂ a) :=
  Option.map_comm h _

Commutativity of Map Composition in `WithBot`

Informal description

For any functions $f_1: \alpha \to \beta$, $f_2: \alpha \to \gamma$, $g_1: \beta \to \delta$, and $g_2: \gamma \to \delta$, if $g_1 \circ f_1 = g_2 \circ f_2$, then for any $a \in \alpha$, the composition of maps on `WithBot` satisfies $\text{map}\, g_1 (\text{map}\, f_1 a) = \text{map}\, g_2 (\text{map}\, f_2 a)$.

WithBot.map₂ definition

: (α → β → γ) → WithBot α → WithBot β → WithBot γ

Full source

/-- The image of a binary function `f : α → β → γ` as a function
`WithBot α → WithBot β → WithBot γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
def map₂ : (α → β → γ) → WithBot α → WithBot β → WithBot γ := Option.map₂

Binary map on `WithBot` type

Informal description

Given a binary function $ f : \alpha \to \beta \to \gamma $, the function `WithBot.map₂` lifts $ f $ to operate on elements of `WithBot α` and `WithBot β`, returning `⊥` (the bottom element) if either input is `⊥` and applying $ f $ to the values otherwise. Mathematically, this corresponds to the image of the function $ f $ viewed as a map $ \alpha \times \beta \to \gamma $, extended to handle the bottom element.

WithBot.map₂_coe_coe theorem

(f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b

Full source

lemma map₂_coe_coe (f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b := rfl

Lifted Binary Map on Non-Bottom Elements Equals Original Function

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and elements $a \in \alpha$, $b \in \beta$, the lifted function `map₂` applied to $f$ and the embeddings of $a$ and $b$ into `WithBot α` and `WithBot β` respectively equals $f(a, b)$. In other words, $\text{map}_2(f, a, b) = f(a, b)$.

WithBot.map₂_bot_left theorem

(f : α → β → γ) (b) : map₂ f ⊥ b = ⊥

Full source

@[simp] lemma map₂_bot_left (f : α → β → γ) (b) : map₂ f ⊥ b = ⊥ := rfl

Lifted Binary Map Preserves Bottom in Left Argument: $\text{map}_2(f, \bot, b) = \bot$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any element $b$ in `WithBot β`, applying the lifted function `map₂` to $f$, the bottom element $\bot$ of `WithBot α`, and $b$ yields the bottom element $\bot$ of `WithBot γ$. That is, $\text{map}_2(f, \bot, b) = \bot$.

WithBot.map₂_bot_right theorem

(f : α → β → γ) (a) : map₂ f a ⊥ = ⊥

Full source

@[simp] lemma map₂_bot_right (f : α → β → γ) (a) : map₂ f a ⊥ = ⊥ := by cases a <;> rfl

Lifted Binary Map Preserves Bottom in Right Argument: $\text{map}_2(f, a, \bot) = \bot$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any element $a$ in `WithBot α`, applying the lifted function `map₂` to $f$, $a$, and the bottom element $\bot$ of `WithBot β$ yields the bottom element $\bot$ of `WithBot γ$. That is, $\text{map}_2(f, a, \bot) = \bot$.

WithBot.map₂_coe_left theorem

(f : α → β → γ) (a : α) (b) : map₂ f a b = b.map fun b ↦ f a b

Full source

@[simp] lemma map₂_coe_left (f : α → β → γ) (a : α) (b) : map₂ f a b = b.map fun b ↦ f a b := rfl

Lifted Binary Map with Left Coefficient: $\text{map}_2(f, a, b) = \text{map}(f(a, \cdot), b)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \alpha$, and any element $b \in \text{WithBot} \beta$, the lifted binary operation $\text{map}_2(f, a, b)$ is equal to applying the function $\lambda b, f(a, b)$ to $b$ in $\text{WithBot} \beta$. In other words, $\text{map}_2(f, a, b) = \text{map}(\lambda b, f(a, b), b)$.

WithBot.map₂_coe_right theorem

(f : α → β → γ) (a) (b : β) : map₂ f a b = a.map (f · b)

Full source

@[simp] lemma map₂_coe_right (f : α → β → γ) (a) (b : β) : map₂ f a b = a.map (f · b) := by
  cases a <;> rfl

Lifted Binary Map with Right Coefficient: $\text{map}_2(f, a, b) = \text{map}(f(\cdot, b), a)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \text{WithBot}\,\alpha$, and any element $b \in \beta$, the lifted binary operation $\text{map}_2(f, a, b)$ is equal to applying the function $f(\cdot, b)$ to $a$ in $\text{WithBot}\,\alpha$. That is, $\text{map}_2(f, a, b) = \text{map}(f(\cdot, b), a)$.

WithBot.map₂_eq_bot_iff theorem

{f : α → β → γ} {a : WithBot α} {b : WithBot β} : map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Full source

@[simp] lemma map₂_eq_bot_iff {f : α → β → γ} {a : WithBot α} {b : WithBot β} :
    map₂map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥ := Option.map₂_eq_none_iff

Bottom Element Characterization in Lifted Binary Operation

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and elements $a \in \text{WithBot}\,\alpha$, $b \in \text{WithBot}\,\beta$, the lifted binary operation $\text{map}_2\,f\,a\,b$ equals the bottom element $\bot$ if and only if either $a = \bot$ or $b = \bot$.

WithBot.ne_bot_iff_exists theorem

{x : WithBot α} : x ≠ ⊥ ↔ ∃ a : α, ↑a = x

Full source

lemma ne_bot_iff_exists {x : WithBot α} : x ≠ ⊥x ≠ ⊥ ↔ ∃ a : α, ↑a = x := Option.ne_none_iff_exists

Non-Bottom Element Characterization in `WithBot α`

Informal description

For any element $x$ in `WithBot α`, $x$ is not equal to the bottom element $\bot$ if and only if there exists an element $a \in \alpha$ such that the canonical embedding of $a$ into `WithBot α` equals $x$.

WithBot.unbot definition

: ∀ x : WithBot α, x ≠ ⊥ → α

Full source

/-- Deconstruct a `x : WithBot α` to the underlying value in `α`, given a proof that `x ≠ ⊥`. -/
def unbot : ∀ x : WithBot α, x ≠ ⊥ → α | (x : α), _ => x

Underlying value in $\alpha$ of a non-bottom element in `WithBot α`

Informal description

Given an element $x$ of type `WithBot α` and a proof that $x \neq \bot$, the function returns the underlying value of $x$ in $\alpha$.

WithBot.coe_unbot theorem

: ∀ (x : WithBot α) hx, x.unbot hx = x

Full source

@[simp] lemma coe_unbot : ∀ (x : WithBot α) hx, x.unbot hx = x | (x : α), _ => rfl

Equality of `unbot` with its Underlying Value in `WithBot α`

Informal description

For any element $x$ of type `WithBot α` and a proof $hx$ that $x \neq \bot$, the underlying value of $x$ in $\alpha$ (obtained via `unbot`) is equal to $x$ itself. In other words, $\text{unbot}(x, hx) = x$.

WithBot.canLift instance

: CanLift (WithBot α) α (↑) fun r => r ≠ ⊥

Full source

instance canLift : CanLift (WithBot α) α (↑) fun r => r ≠ ⊥ where
  prf x h := ⟨x.unbot h, coe_unbot _ _⟩

Lifting Condition for `WithBot α`

Informal description

For any type $\alpha$, there is a canonical way to lift elements from $\alpha$ to `WithBot α` (the type $\alpha$ with an added bottom element $\bot$) via the embedding function, with the condition that the lifted element is not $\bot$.

WithBot.instTop instance

[Top α] : Top (WithBot α)

Full source

instance instTop [Top α] : Top (WithBot α) where
  top := (⊤ : α)

Top Element in `WithBot α` from Top Element in $\alpha$

Informal description

For any type $\alpha$ with a top element $\top$, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) can also be equipped with a top element. This top element in `WithBot α` corresponds to the top element of $\alpha$ when embedded into `WithBot α$.

WithBot.coe_top theorem

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

Full source

@[simp, norm_cast] lemma coe_top [Top α] : ((⊤ : α) : WithBot α) = ⊤ := rfl

Embedding of Top Element Preserves Top in `WithBot α`

Informal description

For any type $\alpha$ with a top element $\top$, the embedding of $\top$ into `WithBot α` (the type $\alpha$ with an added bottom element $\bot$) is equal to the top element in `WithBot α$, i.e., $(\top : \alpha) = \top$ in `WithBot α`.

WithBot.coe_eq_top theorem

[Top α] {a : α} : (a : WithBot α) = ⊤ ↔ a = ⊤

Full source

@[simp, norm_cast] lemma coe_eq_top [Top α] {a : α} : (a : WithBot α) = ⊤ ↔ a = ⊤ := coe_eq_coe

Embedding Equals Top in $\text{WithBot}\,\alpha$ iff Element is Top in $\alpha$

Informal description

For any type $\alpha$ with a top element $\top$ and any element $a \in \alpha$, the canonical embedding of $a$ into $\text{WithBot}\,\alpha$ equals the top element of $\text{WithBot}\,\alpha$ if and only if $a$ equals the top element of $\alpha$. In other words, $(a : \text{WithBot}\,\alpha) = \top \leftrightarrow a = \top$.

WithBot.top_eq_coe theorem

[Top α] {a : α} : ⊤ = (a : WithBot α) ↔ ⊤ = a

Full source

@[simp, norm_cast] lemma top_eq_coe [Top α] {a : α} : ⊤⊤ = (a : WithBot α) ↔ ⊤ = a := coe_eq_coe

Top Equality in $\text{WithBot}\,\alpha$ via Embedding

Informal description

For any type $\alpha$ with a top element $\top$ and any element $a \in \alpha$, the top element of $\text{WithBot}\,\alpha$ equals the canonical embedding of $a$ if and only if $\top$ equals $a$ in $\alpha$. In other words, $\top = (a : \text{WithBot}\,\alpha) \leftrightarrow \top = a$.

WithBot.unbot_eq_iff theorem

{a : WithBot α} {b : α} (h : a ≠ ⊥) : a.unbot h = b ↔ a = b

Full source

theorem unbot_eq_iff {a : WithBot α} {b : α} (h : a ≠ ⊥) :
    a.unbot h = b ↔ a = b := by
  induction a
  · simpa using h rfl
  · simp

Equality of Underlying Value in `WithBot α`

Informal description

For any element $a$ in `WithBot α` that is not the bottom element (i.e., $a \neq \bot$), and for any element $b$ in $\alpha$, the underlying value of $a$ in $\alpha$ (obtained via `unbot`) is equal to $b$ if and only if $a$ is equal to $b$ (when viewed as an element of `WithBot α`).

Equiv.withBotSubtypeNe definition

: { y : WithBot α // y ≠ ⊥ } ≃ α

Full source

/-- The equivalence between the non-bottom elements of `WithBot α` and `α`. -/
@[simps] def _root_.Equiv.withBotSubtypeNe : {y : WithBot α // y ≠ ⊥}{y : WithBot α // y ≠ ⊥} ≃ α where
  toFun := fun ⟨x,h⟩ => WithBot.unbot x h
  invFun x := ⟨x, WithBot.coe_ne_bot⟩
  left_inv _ := by simp
  right_inv _ := by simp

Equivalence between non-bottom elements of `WithBot α` and `α`

Informal description

The equivalence between the subtype of non-bottom elements in `WithBot α` and the type `α` itself. Specifically, it maps a pair `⟨x, h⟩` where `x : WithBot α` and `h : x ≠ ⊥` to the underlying value `x.unbot h` in `α`, and conversely, it maps an element `x : α` to the pair `⟨x, WithBot.coe_ne_bot⟩` in the subtype.

WithBot.le instance

: LE (WithBot α)

Full source

instance (priority := 10) le : LE (WithBot α) :=
  ⟨fun o₁ o₂ => ∀ a : α, o₁ = ↑a → ∃ b : α, o₂ = ↑b ∧ a ≤ b⟩

Preorder Structure on $\alpha$ with Bottom Element

Informal description

For any type $\alpha$ with a preorder, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) inherits a preorder structure where $\bot \leq x$ for all $x \in \text{WithBot }\alpha$, and for $x, y \in \alpha$, $x \leq y$ in `WithBot α` if and only if $x \leq y$ in $\alpha$.

WithBot.le_def theorem

: x ≤ y ↔ ∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b

Full source

lemma le_def : x ≤ y ↔ ∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b := .rfl

Characterization of Inequality in $\text{WithBot }\alpha$ via Embedding of $\alpha$

Informal description

For elements $x$ and $y$ in $\text{WithBot }\alpha$, the inequality $x \leq y$ holds if and only if for every $a \in \alpha$ such that $x = a$, there exists $b \in \alpha$ such that $y = b$ and $a \leq b$ in $\alpha$.

WithBot.coe_le_coe theorem

: (a : WithBot α) ≤ b ↔ a ≤ b

Full source

@[simp, norm_cast] lemma coe_le_coe : (a : WithBot α) ≤ b ↔ a ≤ b := by simp [le_def]

Embedded Inequality Preservation in $\text{WithBot }\alpha$

Informal description

For any elements $a$ and $b$ in $\alpha$, the inequality $a \leq b$ holds in $\text{WithBot }\alpha$ if and only if $a \leq b$ holds in $\alpha$.

WithBot.not_coe_le_bot theorem

(a : α) : ¬(a : WithBot α) ≤ ⊥

Full source

lemma not_coe_le_bot (a : α) : ¬(a : WithBot α) ≤ ⊥ := by simp [le_def]

Embedded Elements Are Not Below Bottom in $\text{WithBot }\alpha$

Informal description

For any element $a$ of type $\alpha$, the embedding of $a$ into $\text{WithBot }\alpha$ is not less than or equal to the bottom element $\bot$.

WithBot.orderBot instance

: OrderBot (WithBot α)

Full source

instance orderBot : OrderBot (WithBot α) where bot_le := by simp [le_def]

Order with Bottom Element on `WithBot α`

Informal description

For any type $\alpha$ with a preorder, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) is an order with a bottom element, where $\bot \leq x$ for all $x \in \text{WithBot }\alpha$.

WithBot.orderTop instance

[OrderTop α] : OrderTop (WithBot α)

Full source

instance orderTop [OrderTop α] : OrderTop (WithBot α) where le_top x := by cases x <;> simp [le_def]

Order Top Structure on $\alpha$ with Bottom Element

Informal description

For any type $\alpha$ with an order and a top element $\top$, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) inherits an order structure where $\top$ from $\alpha$ becomes the top element in `WithBot α`.

WithBot.instBoundedOrder instance

[OrderTop α] : BoundedOrder (WithBot α)

Full source

instance instBoundedOrder [OrderTop α] : BoundedOrder (WithBot α) :=
  { WithBot.orderBot, WithBot.orderTop with }

Bounded Order Structure on `WithBot α` with Top Element

Informal description

For any type $\alpha$ with an order and a top element $\top$, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) is a bounded order, meaning it has both a greatest element (inherited from $\alpha$) and a least element (the added $\bot$).

WithBot.le_bot_iff theorem

: ∀ {a : WithBot α}, a ≤ ⊥ ↔ a = ⊥

Full source

/-- There is a general version `le_bot_iff`, but this lemma does not require a `PartialOrder`. -/
@[simp]
protected theorem le_bot_iff : ∀ {a : WithBot α}, a ≤ ⊥ ↔ a = ⊥
  | (a : α) => by simp [not_coe_le_bot _]
  | ⊥ => by simp

Characterization of Bottom Element in $\text{WithBot }\alpha$: $a \leq \bot \leftrightarrow a = \bot$

Informal description

For any element $a$ in $\text{WithBot }\alpha$, $a \leq \bot$ if and only if $a = \bot$.

WithBot.coe_le theorem

: ∀ {o : Option α}, b ∈ o → ((a : WithBot α) ≤ o ↔ a ≤ b)

Full source

theorem coe_le : ∀ {o : Option α}, b ∈ o → ((a : WithBot α) ≤ o ↔ a ≤ b)
  | _, rfl => coe_le_coe

Embedded Order Relation in `WithBot α` via Option Membership

Informal description

For any element $b$ in an option type `Option α` (viewed as `WithBot α`), if $b$ is a member of the option $o$, then for any element $a$ in `WithBot α`, the inequality $a \leq o$ holds if and only if $a \leq b$ in `WithBot α$.

WithBot.coe_le_iff theorem

: a ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b

Full source

theorem coe_le_iff : a ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b := by simp [le_def]

Characterization of Order Relation in `WithBot α` via Embedding

Informal description

For an element $a$ in `WithBot α` and an element $x$ in `WithBot α$ (where $\alpha$ is a type with a preorder), $a \leq x$ holds if and only if there exists an element $b \in \alpha$ such that $x = b$ (i.e., $x$ is the embedding of $b$ into `WithBot α`) and $a \leq b$ in `WithBot α`.

WithBot.le_coe_iff theorem

: x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b

Full source

theorem le_coe_iff : x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b := by simp [le_def]

Characterization of Order Relation in `WithBot α` via Embedding (Reverse Direction)

Informal description

For an element $x$ in `WithBot α` and an element $b$ in $\alpha$, $x \leq b$ holds if and only if for every $a \in \alpha$ such that $x$ is the embedding of $a$ into `WithBot α` (i.e., $x = a$), we have $a \leq b$ in $\alpha$.

IsMax.withBot theorem

(h : IsMax a) : IsMax (a : WithBot α)

Full source

protected theorem _root_.IsMax.withBot (h : IsMax a) : IsMax (a : WithBot α) :=
  fun x ↦ by cases x <;> simp; simpa using @h _

Maximality Preservation in `WithBot α`

Informal description

If an element $a$ in a preorder $\alpha$ is maximal (i.e., for any $b \in \alpha$, $a \leq b$ implies $b \leq a$), then its image in `WithBot α` (the type $\alpha$ with an added bottom element $\bot$) is also maximal.

WithBot.le_unbot_iff theorem

(hy : y ≠ ⊥) : a ≤ unbot y hy ↔ a ≤ y

Full source

lemma le_unbot_iff (hy : y ≠ ⊥) : a ≤ unbot y hy ↔ a ≤ y := by lift y to α using id hy; simp

Inequality Characterization for Underlying Values in `WithBot α`

Informal description

For any element $y$ in `WithBot α` (the type $\alpha$ with an added bottom element $\bot$) such that $y \neq \bot$, and for any element $a$ in $\alpha$, the inequality $a \leq \text{unbot}(y, hy)$ holds if and only if $a \leq y$ holds in `WithBot α`. Here, $\text{unbot}(y, hy)$ is the underlying value of $y$ in $\alpha$ (given the proof $hy$ that $y \neq \bot$).

WithBot.unbot_le_iff theorem

(hx : x ≠ ⊥) : unbot x hx ≤ b ↔ x ≤ b

Full source

lemma unbot_le_iff (hx : x ≠ ⊥) : unbotunbot x hx ≤ b ↔ x ≤ b := by lift x to α using id hx; simp

Inequality Characterization for Underlying Values in `WithBot α`

Informal description

For any element $x$ of type `WithBot α` (where $\alpha$ is an ordered type) and any element $b \in \alpha$, if $x \neq \bot$, then the inequality $\text{unbot}(x) \leq b$ holds if and only if $x \leq b$, where $\text{unbot}(x)$ is the underlying value of $x$ in $\alpha$.

WithBot.unbotD_le_iff theorem

(hx : x = ⊥ → a ≤ b) : x.unbotD a ≤ b ↔ x ≤ b

Full source

lemma unbotD_le_iff (hx : x = ⊥ → a ≤ b) : x.unbotD a ≤ b ↔ x ≤ b := by cases x <;> simp [hx]

Inequality Characterization for `WithBot.unbotD`

Informal description

For any element $x$ of type `WithBot α` (where $\alpha$ is an ordered type) and any elements $a, b \in \alpha$, if the condition $x = \bot \to a \leq b$ holds, then the inequality $\text{unbotD}(x, a) \leq b$ is equivalent to $x \leq b$. Here, $\text{unbotD}(x, a)$ is defined as $a$ when $x = \bot$ and as the embedded value of $x$ otherwise.

WithBot.lt instance

: LT (WithBot α)

Full source

instance (priority := 10) lt : LT (WithBot α) :=
  ⟨fun o₁ o₂ : WithBot α => ∃ b : α, o₂ = ↑b ∧ ∀ a : α, o₁ = ↑a → a < b⟩

The Less-Than Relation on `WithBot α`

Informal description

For any type $\alpha$ with an order, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) is equipped with a canonical less-than relation.

WithBot.lt_def theorem

: x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b

Full source

lemma lt_def : x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b := .rfl

Characterization of Less-Than Relation in `WithBot α`

Informal description

For elements $x$ and $y$ in `WithBot α` (where $\alpha$ is an ordered type), the relation $x < y$ holds if and only if there exists an element $b \in \alpha$ such that $y$ is the embedding of $b$ into `WithBot α` (i.e., $y = b$) and for every $a \in \alpha$, if $x$ is the embedding of $a$ (i.e., $x = a$), then $a < b$ in $\alpha$.

WithBot.coe_lt_coe theorem

: (a : WithBot α) < b ↔ a < b

Full source

@[simp, norm_cast] lemma coe_lt_coe : (a : WithBot α) < b ↔ a < b := by simp [lt_def]

Embedding Preserves Order in `WithBot α`

Informal description

For any elements $a$ and $b$ of type $\alpha$, the embedding of $a$ into `WithBot α` is less than the embedding of $b$ into `WithBot α$ if and only if $a < b$ in $\alpha$.

WithBot.bot_lt_coe theorem

(a : α) : ⊥ < (a : WithBot α)

Full source

@[simp] lemma bot_lt_coe (a : α) : ⊥ < (a : WithBot α) := by simp [lt_def]

Bottom Element is Less Than Any Embedded Element in `WithBot α`

Informal description

For any element $a$ of type $\alpha$, the bottom element $\bot$ in `WithBot α` is strictly less than the embedding of $a$ into `WithBot α$.

WithBot.not_lt_bot theorem

(a : WithBot α) : ¬a < ⊥

Full source

@[simp] protected lemma not_lt_bot (a : WithBot α) : ¬a < ⊥ := by simp [lt_def]

No Element is Less Than Bottom in `WithBot α`

Informal description

For any element $a$ in `WithBot α` (where $\alpha$ is an ordered type with a bottom element $\bot$), it is not true that $a < \bot$.

WithBot.lt_iff_exists_coe theorem

: x < y ↔ ∃ b : α, y = b ∧ x < b

Full source

lemma lt_iff_exists_coe : x < y ↔ ∃ b : α, y = b ∧ x < b := by cases y <;> simp

Characterization of Less-Than Relation in `WithBot α` via Embedded Elements

Informal description

For any elements $x, y$ in `WithBot α` (where $\alpha$ is an ordered type), the relation $x < y$ holds if and only if there exists an element $b \in \alpha$ such that $y$ is the embedding of $b$ into `WithBot α` and $x < b$ in `WithBot α$.

WithBot.lt_coe_iff theorem

: x < b ↔ ∀ a : α, x = a → a < b

Full source

lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b := by simp [lt_def]

Characterization of Less-Than Relation in `WithBot α` via Embedded Elements and Comparison in $\alpha$

Informal description

For any element $x$ in `WithBot α` and any element $b$ in $\alpha$, the relation $x < b$ holds if and only if for every $a \in \alpha$ such that $x$ is the embedding of $a$ into `WithBot α`, we have $a < b$ in $\alpha$.

WithBot.bot_lt_iff_ne_bot theorem

: ⊥ < x ↔ x ≠ ⊥

Full source

/-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
`PartialOrder α`. -/
protected lemma bot_lt_iff_ne_bot : ⊥⊥ < x ↔ x ≠ ⊥ := by cases x <;> simp

Characterization of $\bot < x$ in `WithBot α` via $x \neq \bot$

Informal description

For any element $x$ in `WithBot α`, the bottom element $\bot$ is less than $x$ if and only if $x$ is not equal to $\bot$.

WithBot.lt_unbot_iff theorem

(hy : y ≠ ⊥) : a < unbot y hy ↔ a < y

Full source

lemma lt_unbot_iff (hy : y ≠ ⊥) : a < unbot y hy ↔ a < y := by lift y to α using id hy; simp

Comparison of Extracted Value in `WithBot α`

Informal description

For any element $y$ in `WithBot α` such that $y \neq \bot$, and for any element $a$ in $\alpha$, the inequality $a < \text{unbot } y \text{ hy}$ holds if and only if $a < y$ in `WithBot α`.

WithBot.unbot_lt_iff theorem

(hx : x ≠ ⊥) : unbot x hx < b ↔ x < b

Full source

lemma unbot_lt_iff (hx : x ≠ ⊥) : unbotunbot x hx < b ↔ x < b := by lift x to α using id hx; simp

Comparison of Underlying Value in `WithBot α`

Informal description

For any element $x$ in `WithBot α` that is not the bottom element (i.e., $x \neq \bot$), and for any element $b$ in `WithBot α`, the underlying value of $x$ in $\alpha$ is less than $b$ if and only if $x$ is less than $b$ in `WithBot α$.

WithBot.unbotD_lt_iff theorem

(hx : x = ⊥ → a < b) : x.unbotD a < b ↔ x < b

Full source

lemma unbotD_lt_iff (hx : x = ⊥ → a < b) : x.unbotD a < b ↔ x < b := by cases x <;> simp [hx]

Comparison of Default-Extracted Value in $\text{WithBot }\alpha$

Informal description

Let $\alpha$ be a type with a preorder, and let $x$ be an element of $\text{WithBot }\alpha$ (the type $\alpha$ extended with a bottom element $\bot$). Given a default value $a \in \alpha$ and an element $b \in \alpha$, the following equivalence holds: the default-extracted value of $x$ (which is $a$ if $x = \bot$ and the embedded value of $x$ otherwise) is less than $b$ if and only if $x$ is less than $b$ in $\text{WithBot }\alpha$, under the condition that whenever $x = \bot$, we have $a < b$.

WithBot.preorder instance

[Preorder α] : Preorder (WithBot α)

Full source

instance preorder [Preorder α] : Preorder (WithBot α) where
  lt_iff_le_not_le x y := by cases x <;> cases y <;> simp [lt_iff_le_not_le]
  le_refl x := by cases x <;> simp [le_def]
  le_trans x y z := by cases x <;> cases y <;> cases z <;> simp [le_def]; simpa using le_trans

Preorder Structure on $\alpha$ with Bottom Element

Informal description

For any preorder $\alpha$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) inherits a preorder structure where $\bot \leq x$ for all $x \in \text{WithBot }\alpha$, and for $x, y \in \alpha$, $x \leq y$ in $\text{WithBot }\alpha$ if and only if $x \leq y$ in $\alpha$.

WithBot.partialOrder instance

[PartialOrder α] : PartialOrder (WithBot α)

Full source

instance partialOrder [PartialOrder α] : PartialOrder (WithBot α) where
  le_antisymm x y := by cases x <;> cases y <;> simp [le_def]; simpa using le_antisymm

Partial Order Structure on $\alpha$ with Bottom Element

Informal description

For any partially ordered set $\alpha$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) inherits a partial order structure where $\bot \leq x$ for all $x \in \text{WithBot }\alpha$, and for $x, y \in \alpha$, $x \leq y$ in $\text{WithBot }\alpha$ if and only if $x \leq y$ in $\alpha$.

WithBot.coe_strictMono theorem

: StrictMono (fun (a : α) => (a : WithBot α))

Full source

theorem coe_strictMono : StrictMono (fun (a : α) => (a : WithBot α)) := fun _ _ => coe_lt_coe.2

Strict Monotonicity of the Embedding $\alpha \hookrightarrow \text{WithBot }\alpha$

Informal description

The embedding function $a \mapsto (a : \text{WithBot }\alpha)$ from $\alpha$ to $\text{WithBot }\alpha$ is strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ in $\alpha$, then $(a : \text{WithBot }\alpha) < (b : \text{WithBot }\alpha)$.

WithBot.coe_mono theorem

: Monotone (fun (a : α) => (a : WithBot α))

Full source

theorem coe_mono : Monotone (fun (a : α) => (a : WithBot α)) := fun _ _ => coe_le_coe.2

Monotonicity of the Embedding $\alpha \hookrightarrow \text{WithBot }\alpha$

Informal description

The embedding function $a \mapsto (a : \text{WithBot }\alpha)$ from $\alpha$ to $\text{WithBot }\alpha$ is monotone. That is, for any $a, b \in \alpha$, if $a \leq b$ in $\alpha$, then $(a : \text{WithBot }\alpha) \leq (b : \text{WithBot }\alpha)$.

WithBot.monotone_iff theorem

{f : WithBot α → β} : Monotone f ↔ Monotone (fun a ↦ f a : α → β) ∧ ∀ x : α, f ⊥ ≤ f x

Full source

theorem monotone_iff {f : WithBot α → β} :
    MonotoneMonotone f ↔ Monotone (fun a ↦ f a : α → β) ∧ ∀ x : α, f ⊥ ≤ f x :=
  ⟨fun h ↦ ⟨h.comp WithBot.coe_mono, fun _ ↦ h bot_le⟩, fun h ↦
    WithBot.forall.2
      ⟨WithBot.forall.2 ⟨fun _ => le_rfl, fun x _ => h.2 x⟩, fun _ =>
        WithBot.forall.2 ⟨fun h => (not_coe_le_bot _ h).elim,
          fun _ hle => h.1 (coe_le_coe.1 hle)⟩⟩⟩

Monotonicity Criterion for Functions on $\text{WithBot}\,\alpha$

Informal description

A function $f \colon \text{WithBot}\,\alpha \to \beta$ is monotone if and only if its restriction to $\alpha$ is monotone and $f(\bot) \leq f(x)$ for all $x \in \alpha$.

WithBot.monotone_map_iff theorem

{f : α → β} : Monotone (WithBot.map f) ↔ Monotone f

Full source

@[simp]
theorem monotone_map_iff {f : α → β} : MonotoneMonotone (WithBot.map f) ↔ Monotone f :=
  monotone_iff.trans <| by simp [Monotone]

Monotonicity of Lifted Function on $\text{WithBot}\,\alpha$

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\text{WithBot.map}\, f \colon \text{WithBot}\,\alpha \to \text{WithBot}\,\beta$ is monotone if and only if $f$ is monotone.

WithBot.strictMono_iff theorem

{f : WithBot α → β} : StrictMono f ↔ StrictMono (fun a => f a : α → β) ∧ ∀ x : α, f ⊥ < f x

Full source

theorem strictMono_iff {f : WithBot α → β} :
    StrictMonoStrictMono f ↔ StrictMono (fun a => f a : α → β) ∧ ∀ x : α, f ⊥ < f x :=
  ⟨fun h => ⟨h.comp WithBot.coe_strictMono, fun _ => h (bot_lt_coe _)⟩, fun h =>
    WithBot.forall.2
      ⟨WithBot.forall.2 ⟨flip absurd (lt_irrefl _), fun x _ => h.2 x⟩, fun _ =>
        WithBot.forall.2 ⟨fun h => (not_lt_bot h).elim, fun _ hle => h.1 (coe_lt_coe.1 hle)⟩⟩⟩

Strict Monotonicity Criterion for Functions on $\text{WithBot}\,\alpha$

Informal description

A function $f \colon \text{WithBot}\,\alpha \to \beta$ is strictly monotone if and only if its restriction to $\alpha$ is strictly monotone and for all $x \in \alpha$, the image of the bottom element satisfies $f(\bot) < f(x)$.

WithBot.strictAnti_iff theorem

{f : WithBot α → β} : StrictAnti f ↔ StrictAnti (fun a ↦ f a : α → β) ∧ ∀ x : α, f x < f ⊥

Full source

theorem strictAnti_iff {f : WithBot α → β} :
    StrictAntiStrictAnti f ↔ StrictAnti (fun a ↦ f a : α → β) ∧ ∀ x : α, f x < f ⊥ :=
  strictMono_iff (β := βᵒᵈ)

Strict Antitonicity Criterion for Functions on $\text{WithBot}\,\alpha$

Informal description

A function $f \colon \text{WithBot}\,\alpha \to \beta$ is strictly antitone if and only if its restriction to $\alpha$ is strictly antitone and for all $x \in \alpha$, the image of the bottom element satisfies $f(x) < f(\bot)$.

WithBot.strictMono_map_iff theorem

{f : α → β} : StrictMono (WithBot.map f) ↔ StrictMono f

Full source

@[simp]
theorem strictMono_map_iff {f : α → β} :
    StrictMonoStrictMono (WithBot.map f) ↔ StrictMono f :=
  strictMono_iff.trans <| by simp [StrictMono, bot_lt_coe]

Strict Monotonicity of Lifted Function in $\text{WithBot}\,\alpha$

Informal description

For any function $f \colon \alpha \to \beta$, the lifted function $\text{WithBot.map}\,f \colon \text{WithBot}\,\alpha \to \text{WithBot}\,\beta$ is strictly monotone if and only if $f$ is strictly monotone.

WithBot.map_le_iff theorem

(f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) : x.map f ≤ y.map f ↔ x ≤ y

Full source

lemma map_le_iff (f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
    x.map f ≤ y.map f ↔ x ≤ y := by cases x <;> cases y <;> simp [mono_iff]

Order-Preserving Property of Lifted Function in $\text{WithBot }\alpha$

Informal description

Let $f : \alpha \to \beta$ be a function such that for all $a, b \in \alpha$, $f(a) \leq f(b)$ if and only if $a \leq b$. Then for any $x, y \in \text{WithBot }\alpha$, the inequality $\text{map}(f)(x) \leq \text{map}(f)(y)$ holds if and only if $x \leq y$.

WithBot.le_coe_unbotD theorem

(x : WithBot α) (b : α) : x ≤ x.unbotD b

Full source

theorem le_coe_unbotD (x : WithBot α) (b : α) : x ≤ x.unbotD b := by cases x <;> simp

Inequality for Default Value Extraction in $\text{WithBot }\alpha$

Informal description

For any element $x$ in $\text{WithBot }\alpha$ and any default value $b \in \alpha$, the inequality $x \leq \text{unbotD}(x, b)$ holds, where $\text{unbotD}(x, b)$ is equal to $b$ if $x$ is the bottom element $\bot$, and is equal to the embedded value of $x$ otherwise.

WithBot.lt_coe_bot theorem

[OrderBot α] : x < (⊥ : α) ↔ x = ⊥

Full source

@[simp]
theorem lt_coe_bot [OrderBot α] : x < (⊥ : α) ↔ x = ⊥ := by cases x <;> simp

Characterization of Bottom Element in $\text{WithBot }\alpha$: $x < \bot \leftrightarrow x = \bot$

Informal description

Let $\alpha$ be a type with an order and a bottom element $\bot$. For any element $x$ in $\text{WithBot }\alpha$, the inequality $x < \bot$ holds if and only if $x$ is equal to $\bot$.

WithBot.forall_le_coe_iff_le theorem

[NoBotOrder α] : (∀ a : α, y ≤ a → x ≤ a) ↔ x ≤ y

Full source

lemma forall_le_coe_iff_le [NoBotOrder α] : (∀ a : α, y ≤ a → x ≤ a) ↔ x ≤ y := by
  obtain _ | y := y
  · simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]
  · exact ⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩

Characterization of Order Relation in $\text{WithBot }\alpha$ via Universal Property

Informal description

Let $\alpha$ be a type with a preorder and no bottom element. For any elements $x, y \in \text{WithBot }\alpha$, the following are equivalent: 1. For every $a \in \alpha$, if $y \leq a$ then $x \leq a$. 2. $x \leq y$. Here, $\text{WithBot }\alpha$ denotes the type $\alpha$ extended with a bottom element $\bot$, and the order is extended such that $\bot \leq x$ for all $x \in \text{WithBot }\alpha$.

WithBot.semilatticeSup instance

[SemilatticeSup α] : SemilatticeSup (WithBot α)

Full source

instance semilatticeSup [SemilatticeSup α] : SemilatticeSup (WithBot α) where
  sup
    -- note this is `Option.merge`, but with the right defeq when unfolding
    | ⊥, ⊥ => ⊥
    | (a : α), ⊥ => a
    | ⊥, (b : α) => b
    | (a : α), (b : α) => ↑(a ⊔ b)
  le_sup_left x y := by cases x <;> cases y <;> simp
  le_sup_right x y := by cases x <;> cases y <;> simp
  sup_le x y z := by cases x <;> cases y <;> cases z <;> simp; simpa using sup_le

Join-Semilattice Structure on $\alpha$ with Bottom Element

Informal description

For any join-semilattice $\alpha$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) inherits a join-semilattice structure. The join operation $\sqcup$ on $\text{WithBot }\alpha$ is defined such that: 1. $\bot \sqcup x = x$ for all $x \in \text{WithBot }\alpha$, 2. $x \sqcup \bot = x$ for all $x \in \text{WithBot }\alpha$, 3. For $x, y \in \alpha$, $x \sqcup y$ in $\text{WithBot }\alpha$ is the same as $x \sqcup y$ in $\alpha$.

WithBot.coe_sup theorem

[SemilatticeSup α] (a b : α) : ((a ⊔ b : α) : WithBot α) = (a : WithBot α) ⊔ b

Full source

theorem coe_sup [SemilatticeSup α] (a b : α) : ((a ⊔ b : α) : WithBot α) = (a : WithBot α) ⊔ b :=
  rfl

Embedding Preserves Supremum in $\text{WithBot }\alpha$

Informal description

Let $\alpha$ be a join-semilattice. For any two elements $a, b \in \alpha$, the embedding of their supremum $a \sqcup b$ in $\text{WithBot }\alpha$ is equal to the supremum of their embeddings in $\text{WithBot }\alpha$. That is, $(a \sqcup b : \text{WithBot }\alpha) = (a : \text{WithBot }\alpha) \sqcup (b : \text{WithBot }\alpha)$.

WithBot.semilatticeInf instance

[SemilatticeInf α] : SemilatticeInf (WithBot α)

Full source

instance semilatticeInf [SemilatticeInf α] : SemilatticeInf (WithBot α) where
  inf := .map₂ (· ⊓ ·)
  inf_le_left x y := by cases x <;> cases y <;> simp
  inf_le_right x y := by cases x <;> cases y <;> simp
  le_inf x y z := by cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

Meet-Semilattice Structure on $\alpha$ with Bottom Element

Informal description

For any meet-semilattice $\alpha$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) inherits a meet-semilattice structure. The meet operation is defined such that $\bot \sqcap x = \bot$ for all $x \in \text{WithBot }\alpha$, and for $x, y \in \alpha$, $x \sqcap y$ in $\text{WithBot }\alpha$ is the meet of $x$ and $y$ in $\alpha$.

WithBot.coe_inf theorem

[SemilatticeInf α] (a b : α) : ((a ⊓ b : α) : WithBot α) = (a : WithBot α) ⊓ b

Full source

theorem coe_inf [SemilatticeInf α] (a b : α) : ((a ⊓ b : α) : WithBot α) = (a : WithBot α) ⊓ b :=
  rfl

Embedding Preserves Meet in $\text{WithBot }\alpha$

Informal description

Let $\alpha$ be a meet-semilattice. For any two elements $a, b \in \alpha$, the embedding of their meet $a \sqcap b$ in $\text{WithBot }\alpha$ is equal to the meet of their embeddings in $\text{WithBot }\alpha$. That is, $(a \sqcap b : \text{WithBot }\alpha) = (a : \text{WithBot }\alpha) \sqcap (b : \text{WithBot }\alpha)$.

WithBot.lattice instance

[Lattice α] : Lattice (WithBot α)

Full source

instance lattice [Lattice α] : Lattice (WithBot α) :=
  { WithBot.semilatticeSup, WithBot.semilatticeInf with }

Lattice Structure on $\alpha$ with Adjoined Bottom Element

Informal description

For any lattice $\alpha$, the type $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element $\bot$ to $\alpha$) inherits a lattice structure. The meet and join operations are defined as follows: - For the meet operation $\sqcap$: - $\bot \sqcap x = \bot$ for all $x \in \text{WithBot}\ \alpha$, - For $x, y \in \alpha$, $x \sqcap y$ in $\text{WithBot}\ \alpha$ is the meet of $x$ and $y$ in $\alpha$. - For the join operation $\sqcup$: - $\bot \sqcup x = x$ for all $x \in \text{WithBot}\ \alpha$, - For $x, y \in \alpha$, $x \sqcup y$ in $\text{WithBot}\ \alpha$ is the join of $x$ and $y$ in $\alpha$.

WithBot.distribLattice instance

[DistribLattice α] : DistribLattice (WithBot α)

Full source

instance distribLattice [DistribLattice α] : DistribLattice (WithBot α) where
  le_sup_inf x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_inf, ← coe_sup]
    simpa [← coe_inf, ← coe_sup] using le_sup_inf

Distributive Lattice Structure on $\alpha$ with Adjoined Bottom Element

Informal description

For any distributive lattice $\alpha$, the type $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element $\bot$ to $\alpha$) inherits a distributive lattice structure. The meet and join operations are defined as follows: - For the meet operation $\sqcap$: - $\bot \sqcap x = \bot$ for all $x \in \text{WithBot}\ \alpha$, - For $x, y \in \alpha$, $x \sqcap y$ in $\text{WithBot}\ \alpha$ is the meet of $x$ and $y$ in $\alpha$. - For the join operation $\sqcup$: - $\bot \sqcup x = x$ for all $x \in \text{WithBot}\ \alpha$, - For $x, y \in \alpha$, $x \sqcup y$ in $\text{WithBot}\ \alpha$ is the join of $x$ and $y$ in $\alpha$.

WithBot.decidableEq instance

[DecidableEq α] : DecidableEq (WithBot α)

Full source

instance decidableEq [DecidableEq α] : DecidableEq (WithBot α) :=
  inferInstanceAs <| DecidableEq (Option α)

Decidable Equality for $\text{WithBot}\ \alpha$

Informal description

For any type $\alpha$ with a decidable equality, the type $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element to $\alpha$) also has a decidable equality.

WithBot.decidableLE instance

[LE α] [DecidableLE α] : DecidableLE (WithBot α)

Full source

instance decidableLE [LE α] [DecidableLE α] : DecidableLE (WithBot α)
  | ⊥, _ => isTrue <| by simp
  | (a : α), ⊥ => isFalse <| by simp
  | (a : α), (b : α) => decidable_of_iff' _ coe_le_coe

Decidable Less-Than-or-Equal Relation on $\text{WithBot}\ \alpha$

Informal description

For any type $\alpha$ with a decidable less-than-or-equal-to relation, the type $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element to $\alpha$) also has a decidable less-than-or-equal-to relation.

WithBot.decidableLT instance

[LT α] [DecidableLT α] : DecidableLT (WithBot α)

Full source

instance decidableLT [LT α] [DecidableLT α] : DecidableLT (WithBot α)
  | _, ⊥ => isFalse <| by simp
  | ⊥, (a : α) => isTrue <| by simp
  | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe

Decidable Less-Than Relation on $\text{WithBot}\ \alpha$

Informal description

For any type $\alpha$ with a decidable less-than relation, the type $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element to $\alpha$) also has a decidable less-than relation.

WithBot.isTotal_le instance

[LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithBot α) (· ≤ ·)

Full source

instance isTotal_le [LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithBot α) (· ≤ ·) where
  total x y := by cases x <;> cases y <;> simp; simpa using IsTotal.total ..

Total Order on $\text{WithBot}\ \alpha$ Inherited from $\alpha$

Informal description

For any type $\alpha$ with a total order $\leq$, the order $\leq$ on $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element $\bot$ to $\alpha$) is also total. That is, for any two elements $x, y \in \text{WithBot}\ \alpha$, either $x \leq y$ or $y \leq x$ holds.

WithBot.linearOrder instance

: LinearOrder (WithBot α)

Full source

instance linearOrder : LinearOrder (WithBot α) := Lattice.toLinearOrder _

Linear Order on $\alpha$ with Adjoined Bottom Element

Informal description

For any linearly ordered type $\alpha$, the type $\text{WithBot}\ \alpha$ (obtained by adjoining a bottom element $\bot$ to $\alpha$) inherits a linear order structure. The order relation is defined by extending the order on $\alpha$ with $\bot$ as the smallest element.

WithBot.coe_min theorem

(a b : α) : ↑(min a b) = min (a : WithBot α) b

Full source

@[simp, norm_cast] lemma coe_min (a b : α) : ↑(min a b) = min (a : WithBot α) b := rfl

Embedding Preserves Minimum in $\text{WithBot}\ \alpha$

Informal description

For any two elements $a$ and $b$ in a type $\alpha$, the embedding of their minimum $\min(a, b)$ into $\text{WithBot}\ \alpha$ (via the coercion map $\uparrow$) equals the minimum of their embeddings $\min(\uparrow a, \uparrow b)$ in $\text{WithBot}\ \alpha$.

WithBot.coe_max theorem

(a b : α) : ↑(max a b) = max (a : WithBot α) b

Full source

@[simp, norm_cast] lemma coe_max (a b : α) : ↑(max a b) = max (a : WithBot α) b := rfl

Embedding Preserves Maximum in $\text{WithBot }\alpha$

Informal description

For any two elements $a$ and $b$ in a type $\alpha$, the embedding of their maximum $\max(a, b)$ into $\text{WithBot }\alpha$ (the type $\alpha$ with an added bottom element $\bot$) is equal to the maximum of their embeddings in $\text{WithBot }\alpha$. That is, $\uparrow(\max(a, b)) = \max(\uparrow a, \uparrow b)$.

WithBot.le_of_forall_lt_iff_le theorem

: (∀ z : α, x < z → y ≤ z) ↔ y ≤ x

Full source

lemma le_of_forall_lt_iff_le : (∀ z : α, x < z → y ≤ z) ↔ y ≤ x := by
  cases x <;> cases y <;> simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

Characterization of Order Relation in `WithBot α` via Forall-Implication

Informal description

For elements $x, y$ in `WithBot α`, the following are equivalent: 1. For all $z \in \alpha$, if $x < z$ then $y \leq z$. 2. $y \leq x$. Here, `WithBot α` is the type obtained by adjoining a bottom element $\bot$ to $\alpha$, and the order is extended such that $\bot \leq x$ for all $x \in \text{WithBot }\alpha$.

WithBot.ge_of_forall_gt_iff_ge theorem

: (∀ z : α, z < x → z ≤ y) ↔ x ≤ y

Full source

lemma ge_of_forall_gt_iff_ge : (∀ z : α, z < x → z ≤ y) ↔ x ≤ y := by
  cases x <;> cases y <;> simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Characterization of Order Relation in $\text{WithBot }\alpha$ via Strict Comparisons

Informal description

For elements $x$ and $y$ in $\text{WithBot }\alpha$, the following are equivalent: 1. For every $z \in \alpha$, if $z < x$ then $z \leq y$. 2. $x \leq y$.

WithBot.instWellFoundedLT instance

[LT α] [WellFoundedLT α] : WellFoundedLT (WithBot α)

Full source

instance instWellFoundedLT [LT α] [WellFoundedLT α] : WellFoundedLT (WithBot α) where
  wf := .intro fun
  | ⊥ => ⟨_, by simp⟩
  | (a : α) => (wellFounded_lt.1 a).rec fun _ _ ih ↦ .intro _ fun
    | ⊥, _ => ⟨_, by simp⟩
    | (b : α), hlt => ih _ (coe_lt_coe.1 hlt)

Well-Foundedness of the Less-Than Relation on `WithBot α`

Informal description

For any type $\alpha$ with a well-founded less-than relation, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) also has a well-founded less-than relation.

WithBot.instWellFoundedGT instance

[LT α] [WellFoundedGT α] : WellFoundedGT (WithBot α)

Full source

instance _root_.WithBot.instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithBot α) where
  wf :=
  have acc_some (a : α) : Acc ((· > ·) : WithBot α → WithBot α → Prop) a :=
    (wellFounded_gt.1 a).rec fun _ _ ih =>
      .intro _ fun
        | (b : α), hlt => ih _ (coe_lt_coe.1 hlt)
  .intro fun
    | (a : α) => acc_some a
    | ⊥ => .intro _ fun | (b : α), _ => acc_some b

Well-Founded Greater-Than Relation on `WithBot α`

Informal description

For any type $\alpha$ with a well-founded greater-than relation, the type `WithBot α` (which is $\alpha$ with an added bottom element $\bot$) also has a well-founded greater-than relation.

WithBot.denselyOrdered instance

[LT α] [DenselyOrdered α] [NoMinOrder α] : DenselyOrdered (WithBot α)

Full source

instance denselyOrdered [LT α] [DenselyOrdered α] [NoMinOrder α] : DenselyOrdered (WithBot α) where
  dense := fun
    | ⊥, (b : α), _ =>
      let ⟨a, ha⟩ := exists_lt b
      ⟨a, by simpa⟩
    | (a : α), (b : α), hab =>
      let ⟨c, hac, hcb⟩ := exists_between (coe_lt_coe.1 hab)
      ⟨c, coe_lt_coe.2 hac, coe_lt_coe.2 hcb⟩

Densely Ordered Structure on $\text{WithBot}\ \alpha$

Informal description

For any densely ordered type $\alpha$ with no minimal elements, the type $\text{WithBot}\ \alpha$ (which is $\alpha$ with an added bottom element $\bot$) is also densely ordered. This means that for any two elements $a < b$ in $\text{WithBot}\ \alpha$, there exists an element $x$ such that $a < x < b$.

WithBot.lt_iff_exists_coe_btwn theorem

[Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} : a < b ↔ ∃ x : α, a < ↑x ∧ ↑x < b

Full source

theorem lt_iff_exists_coe_btwn [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} :
    a < b ↔ ∃ x : α, a < ↑x ∧ ↑x < b :=
  ⟨fun h =>
    let ⟨_, hy⟩ := exists_between h
    let ⟨x, hx⟩ := lt_iff_exists_coe.1 hy.1
    ⟨x, hx.1 ▸ hy⟩,
    fun ⟨_, hx⟩ => lt_trans hx.1 hx.2⟩

Characterization of Order in $\text{WithBot}\ \alpha$ via Intermediate Elements

Informal description

Let $\alpha$ be a preorder that is densely ordered and has no minimal elements. For any two elements $a, b$ in $\text{WithBot}\ \alpha$, the relation $a < b$ holds if and only if there exists an element $x \in \alpha$ such that $a < x$ and $x < b$ in $\text{WithBot}\ \alpha$.

WithBot.noTopOrder instance

[LE α] [NoTopOrder α] [Nonempty α] : NoTopOrder (WithBot α)

Full source

instance noTopOrder [LE α] [NoTopOrder α] [Nonempty α] : NoTopOrder (WithBot α) where
  exists_not_le := fun
    | ⊥ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) => let ⟨b, hba⟩ := exists_not_le a; ⟨b, mod_cast hba⟩

No Top Elements in $\text{WithBot}\ \alpha$

Informal description

For any nonempty type $\alpha$ with a preorder and no top elements, the type $\text{WithBot}\ \alpha$ (which is $\alpha$ with an added bottom element $\bot$) also has no top elements.

WithBot.noMaxOrder instance

[LT α] [NoMaxOrder α] [Nonempty α] : NoMaxOrder (WithBot α)

Full source

instance noMaxOrder [LT α] [NoMaxOrder α] [Nonempty α] : NoMaxOrder (WithBot α) where
  exists_gt := fun
    | ⊥ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) => let ⟨b, hba⟩ := exists_gt a; ⟨b, mod_cast hba⟩

No Maximal Elements in $\text{WithBot}\ \alpha$

Informal description

For any type $\alpha$ with a strict order and no maximal elements, and which is nonempty, the type $\text{WithBot}\ \alpha$ (which is $\alpha$ with an added bottom element $\bot$) also has no maximal elements.

WithTop.nontrivial instance

[Nonempty α] : Nontrivial (WithTop α)

Full source

instance nontrivial [Nonempty α] : Nontrivial (WithTop α) :=
  Option.nontrivial

Nontriviality of $\text{WithTop}\ \alpha$ for Nonempty $\alpha$

Informal description

For any nonempty type $\alpha$, the type $\text{WithTop}\ \alpha$ (which is $\alpha$ extended with a top element $\top$) is nontrivial, meaning it contains at least two distinct elements.

WithTop.coe_injective theorem

: Injective ((↑) : α → WithTop α)

Full source

theorem coe_injective : Injective ((↑) : α → WithTop α) :=
  Option.some_injective _

Injectivity of the Canonical Injection into $\text{WithTop}\ \alpha$

Informal description

The canonical injection function $(↑) : \alpha \to \text{WithTop}\ \alpha$ is injective. That is, for any $a, b \in \alpha$, if $a = b$ in $\text{WithTop}\ \alpha$, then $a = b$ in $\alpha$.

WithTop.coe_inj theorem

: (a : WithTop α) = b ↔ a = b

Full source

@[norm_cast]
theorem coe_inj : (a : WithTop α) = b ↔ a = b :=
  Option.some_inj

Injectivity of Canonical Injection into $\text{WithTop}\ \alpha$

Informal description

For any elements $a, b$ in a type $\alpha$, the canonical injections $\text{some}\ a$ and $\text{some}\ b$ into $\text{WithTop}\ \alpha$ are equal if and only if $a = b$.

WithTop.forall theorem

{p : WithTop α → Prop} : (∀ x, p x) ↔ p ⊤ ∧ ∀ x : α, p x

Full source

protected theorem «forall» {p : WithTop α → Prop} : (∀ x, p x) ↔ p ⊤ ∧ ∀ x : α, p x :=
  Option.forall

Universal Quantification over $\text{WithTop}\ \alpha$ Decomposes into Top and Base Cases

Informal description

For any predicate $p$ on $\text{WithTop}\ \alpha$, the universal quantification $\forall x, p(x)$ holds if and only if $p(\top)$ holds and $p(x)$ holds for all $x \in \alpha$.

WithTop.exists theorem

{p : WithTop α → Prop} : (∃ x, p x) ↔ p ⊤ ∨ ∃ x : α, p x

Full source

protected theorem «exists» {p : WithTop α → Prop} : (∃ x, p x) ↔ p ⊤ ∨ ∃ x : α, p x :=
  Option.exists

Existential Quantification over $\text{WithTop}\ \alpha$ Decomposes into Top and Base Cases

Informal description

For any predicate $p$ on $\text{WithTop}\ \alpha$, there exists an element $x$ in $\text{WithTop}\ \alpha$ satisfying $p(x)$ if and only if either $p(\top)$ holds or there exists an element $x \in \alpha$ such that $p(x)$ holds.

WithTop.none_eq_top theorem

: (none : WithTop α) = (⊤ : WithTop α)

Full source

theorem none_eq_top : (none : WithTop α) = (⊤ : WithTop α) :=
  rfl

Equality of `none` and top in `WithTop`

Informal description

In the type `WithTop α` (the extension of type `α` with a top element), the `none` value is equal to the top element $\top$.

WithTop.some_eq_coe theorem

(a : α) : (Option.some a : WithTop α) = (↑a : WithTop α)

Full source

theorem some_eq_coe (a : α) : (Option.some a : WithTop α) = (↑a : WithTop α) :=
  rfl

Equality of Some and Canonical Embedding in WithTop

Informal description

For any element $a$ of type $\alpha$, the injection of $a$ into $\text{WithTop}\ \alpha$ via `Option.some` is equal to the canonical embedding of $a$ into $\text{WithTop}\ \alpha$, i.e., $\text{some}\ a = a$.

WithTop.top_ne_coe theorem

: ⊤ ≠ (a : WithTop α)

Full source

@[simp]
theorem top_ne_coe : ⊤⊤ ≠ (a : WithTop α) :=
  nofun

Top element is distinct from embedded elements in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ of type $\alpha$, the top element $\top$ in $\text{WithTop}\ \alpha$ is not equal to the canonical embedding of $a$ into $\text{WithTop}\ \alpha$.

WithTop.coe_ne_top theorem

: (a : WithTop α) ≠ ⊤

Full source

@[simp]
theorem coe_ne_top : (a : WithTop α) ≠ ⊤ :=
  nofun

Embedded Element is Not Top in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ of type $\alpha$, the canonical embedding of $a$ into $\text{WithTop}\ \alpha$ is not equal to the top element $\top$.

WithTop.toDual definition

: WithTop α ≃ WithBot αᵒᵈ

Full source

/-- `WithTop.toDual` is the equivalence sending `⊤` to `⊥` and any `a : α` to `toDual a : αᵒᵈ`.
See `WithTop.toDualBotEquiv` for the related order-iso.
-/
protected def toDual : WithTopWithTop α ≃ WithBot αᵒᵈ :=
  Equiv.refl _

Equivalence between `WithTop α` and `WithBot αᵒᵈ`

Informal description

The equivalence `WithTop.toDual` maps the top element $\top$ of `WithTop α` to the bottom element $\bot$ of `WithBot αᵒᵈ$, and any element $a : α$ to its corresponding dual element `toDual a : αᵒᵈ` in `WithBot αᵒᵈ`. This establishes a bijection between `WithTop α` and `WithBot αᵒᵈ`.

WithTop.ofDual definition

: WithTop αᵒᵈ ≃ WithBot α

Full source

/-- `WithTop.ofDual` is the equivalence sending `⊤` to `⊥` and any `a : αᵒᵈ` to `ofDual a : α`.
See `WithTop.toDualBotEquiv` for the related order-iso.
-/
protected def ofDual : WithTopWithTop αᵒᵈ ≃ WithBot α :=
  Equiv.refl _

Equivalence between `WithTop αᵒᵈ` and `WithBot α`

Informal description

The equivalence `WithTop.ofDual` maps the top element `⊤` of `WithTop αᵒᵈ` to the bottom element `⊥` of `WithBot α`, and any element `a : αᵒᵈ` to its corresponding element `ofDual a : α` in `WithBot α`. This establishes a bijection between `WithTop αᵒᵈ` and `WithBot α`.

WithBot.toDual definition

: WithBot α ≃ WithTop αᵒᵈ

Full source

/-- `WithBot.toDual` is the equivalence sending `⊥` to `⊤` and any `a : α` to `toDual a : αᵒᵈ`.
See `WithBot.toDual_top_equiv` for the related order-iso.
-/
protected def _root_.WithBot.toDual : WithBotWithBot α ≃ WithTop αᵒᵈ :=
  Equiv.refl _

Equivalence between `WithBot α` and `WithTop αᵒᵈ`

Informal description

The equivalence `WithBot.toDual` maps the bottom element `⊥` of `WithBot α` to the top element `⊤` of `WithTop αᵒᵈ`, and any element `a : α` to its corresponding dual element `toDual a : αᵒᵈ` in `WithTop αᵒᵈ`. This establishes a bijection between `WithBot α` and `WithTop αᵒᵈ`.

WithBot.ofDual definition

: WithBot αᵒᵈ ≃ WithTop α

Full source

/-- `WithBot.ofDual` is the equivalence sending `⊥` to `⊤` and any `a : αᵒᵈ` to `ofDual a : α`.
See `WithBot.ofDual_top_equiv` for the related order-iso.
-/
protected def _root_.WithBot.ofDual : WithBotWithBot αᵒᵈ ≃ WithTop α :=
  Equiv.refl _

Equivalence between `WithBot αᵒᵈ` and `WithTop α`

Informal description

The equivalence `WithBot.ofDual` maps the bottom element `⊥` of `WithBot αᵒᵈ` to the top element `⊤` of `WithTop α`, and any element `a : αᵒᵈ` to its corresponding element `ofDual a : α` in `WithTop α`. This establishes a bijection between `WithBot αᵒᵈ` and `WithTop α`.

WithTop.toDual_symm_apply theorem

(a : WithBot αᵒᵈ) : WithTop.toDual.symm a = WithBot.ofDual a

Full source

@[simp]
theorem toDual_symm_apply (a : WithBot αᵒᵈ) : WithTop.toDual.symm a = WithBot.ofDual a :=
  rfl

Inverse of WithTop.toDual Equals WithBot.ofDual

Informal description

For any element $a$ in $\text{WithBot} \, \alpha^\text{op}$, the inverse of the equivalence $\text{WithTop.toDual}$ applied to $a$ is equal to $\text{WithBot.ofDual}$ applied to $a$. In other words, $(\text{WithTop.toDual})^{-1}(a) = \text{WithBot.ofDual}(a)$.

WithTop.ofDual_symm_apply theorem

(a : WithBot α) : WithTop.ofDual.symm a = WithBot.toDual a

Full source

@[simp]
theorem ofDual_symm_apply (a : WithBot α) : WithTop.ofDual.symm a = WithBot.toDual a :=
  rfl

Inverse of `WithTop.ofDual` Equals `WithBot.toDual`

Informal description

For any element $a$ in `WithBot α`, the inverse of the equivalence `WithTop.ofDual` maps $a$ to the equivalence `WithBot.toDual` applied to $a$. In other words, the inverse of the bijection between `WithTop αᵒᵈ` and `WithBot α` is given by the bijection between `WithBot α` and `WithTop αᵒᵈ`.

WithTop.toDual_apply_top theorem

: WithTop.toDual (⊤ : WithTop α) = ⊥

Full source

@[simp]
theorem toDual_apply_top : WithTop.toDual (⊤ : WithTop α) = ⊥ :=
  rfl

Top-to-Bottom Mapping via Duality: $\text{toDual}(\top) = \bot$

Informal description

The equivalence `WithTop.toDual` maps the top element $\top$ of `WithTop α` to the bottom element $\bot$ of `WithBot αᵒᵈ$.

WithTop.ofDual_apply_top theorem

: WithTop.ofDual (⊤ : WithTop α) = ⊥

Full source

@[simp]
theorem ofDual_apply_top : WithTop.ofDual (⊤ : WithTop α) = ⊥ :=
  rfl

Mapping of Top Element to Bottom Element via Dual Equivalence

Informal description

The equivalence `WithTop.ofDual` maps the top element $\top$ of the type `WithTop α` to the bottom element $\bot$ of the type `WithBot α`, i.e., $\text{WithTop.ofDual}(\top) = \bot$.

WithTop.toDual_apply_coe theorem

(a : α) : WithTop.toDual (a : WithTop α) = toDual a

Full source

@[simp]
theorem toDual_apply_coe (a : α) : WithTop.toDual (a : WithTop α) = toDual a :=
  rfl

Equivalence of `WithTop.toDual` on elements of $\alpha$

Informal description

For any element $a$ of type $\alpha$, the equivalence `WithTop.toDual` maps the element $a$ in `WithTop α` to its dual element in `WithBot αᵒᵈ$, i.e., $\text{WithTop.toDual}(a) = \text{toDual}(a)$.

WithTop.ofDual_apply_coe theorem

(a : αᵒᵈ) : WithTop.ofDual (a : WithTop αᵒᵈ) = ofDual a

Full source

@[simp]
theorem ofDual_apply_coe (a : αᵒᵈ) : WithTop.ofDual (a : WithTop αᵒᵈ) = ofDual a :=
  rfl

Equivalence between `WithTop αᵒᵈ` and `WithBot α` on elements

Informal description

For any element $a$ in the order dual of $\alpha$, the equivalence `WithTop.ofDual` maps the element `a` in `WithTop αᵒᵈ` to the element `ofDual a` in `WithBot α`.

WithTop.untopD definition

(d : α) (x : WithTop α) : α

Full source

/-- Specialization of `Option.getD` to values in `WithTop α` that respects API boundaries.
-/
def untopD (d : α) (x : WithTop α) : α :=
  recTopCoe d id x

Default value extraction from `WithTop`

Informal description

The function `WithTop.untopD` takes a default value `d : α` and an element `x : WithTop α`, and returns `d` if `x` is the top element `⊤`, or the underlying value of `x` if `x` is of the form `↑a` for some `a : α`.

WithTop.untopD_top theorem

{α} (d : α) : untopD d ⊤ = d

Full source

@[simp]
theorem untopD_top {α} (d : α) : untopD d ⊤ = d :=
  rfl

Default Extraction of Top Element in $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ and element $d \in \alpha$, the function $\text{untopD}$ satisfies $\text{untopD}\ d\ \top = d$.

WithTop.untopD_coe theorem

{α} (d x : α) : untopD d x = x

Full source

@[simp]
theorem untopD_coe {α} (d x : α) : untopD d x = x :=
  rfl

Default Extraction Preserves Injected Elements in $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ and elements $d, x \in \alpha$, the function `untopD` satisfies $\text{untopD}\ d\ x = x$.

WithTop.coe_eq_coe theorem

: (a : WithTop α) = b ↔ a = b

Full source

@[simp, norm_cast]
theorem coe_eq_coe : (a : WithTop α) = b ↔ a = b :=
  Option.some_inj

Equality of Injected Elements in $\text{WithTop}\ \alpha$

Informal description

For any elements $a, b \in \alpha$, the equality $\text{some}\ a = \text{some}\ b$ holds in $\text{WithTop}\ \alpha$ if and only if $a = b$ holds in $\alpha$.

WithTop.untopD_eq_iff theorem

{d y : α} {x : WithTop α} : untopD d x = y ↔ x = y ∨ x = ⊤ ∧ y = d

Full source

theorem untopD_eq_iff {d y : α} {x : WithTop α} : untopDuntopD d x = y ↔ x = y ∨ x = ⊤ ∧ y = d :=
  WithBot.unbotD_eq_iff

Characterization of Equality for Default Value Extraction in $\text{WithTop}\,\alpha$

Informal description

For any default value $d$ and element $y$ in $\alpha$, and for any element $x$ in $\text{WithTop}\,\alpha$, the equality $\text{untopD}\,d\,x = y$ holds if and only if either $x$ is equal to $y$ (as embedded elements), or $x$ is the top element $\top$ and $y$ equals the default value $d$.

WithTop.untopD_eq_self_iff theorem

{d : α} {x : WithTop α} : untopD d x = d ↔ x = d ∨ x = ⊤

Full source

@[simp]
theorem untopD_eq_self_iff {d : α} {x : WithTop α} : untopDuntopD d x = d ↔ x = d ∨ x = ⊤ :=
  WithBot.unbotD_eq_self_iff

Characterization of Default Value Extraction in $\text{WithTop}\,\alpha$

Informal description

For any default value $d$ in $\alpha$ and any element $x$ in $\text{WithTop}\,\alpha$, the equality $\text{untopD}\,d\,x = d$ holds if and only if either $x$ is equal to $d$ (as an embedded element) or $x$ is the top element $\top$.

WithTop.untopD_eq_untopD_iff theorem

{d : α} {x y : WithTop α} : untopD d x = untopD d y ↔ x = y ∨ x = d ∧ y = ⊤ ∨ x = ⊤ ∧ y = d

Full source

theorem untopD_eq_untopD_iff {d : α} {x y : WithTop α} :
    untopDuntopD d x = untopD d y ↔ x = y ∨ x = d ∧ y = ⊤ ∨ x = ⊤ ∧ y = d :=
  WithBot.unbotD_eq_unbotD_iff

Equality Condition for Default Value Extraction in $\text{WithTop}\,\alpha$

Informal description

For any default value $d$ in $\alpha$ and elements $x, y$ in $\text{WithTop}\,\alpha$, the equality $\text{untopD}\,d\,x = \text{untopD}\,d\,y$ holds if and only if either $x = y$, or $x = d$ and $y = \top$, or $x = \top$ and $y = d$.

WithTop.map definition

(f : α → β) : WithTop α → WithTop β

Full source

/-- Lift a map `f : α → β` to `WithTop α → WithTop β`. Implemented using `Option.map`. -/
def map (f : α → β) : WithTop α → WithTop β :=
  Option.map f

Lifting a map to `WithTop`

Informal description

The function lifts a map $f : \alpha \to \beta$ to a map $\text{WithTop}\ \alpha \to \text{WithTop}\ \beta$ by applying $f$ to the elements of $\alpha$ and mapping the top element $\top$ to itself. Formally, this is implemented using the `Option.map` function.

WithTop.map_top theorem

(f : α → β) : map f ⊤ = ⊤

Full source

@[simp]
theorem map_top (f : α → β) : map f ⊤ = ⊤ :=
  rfl

Top Element Preservation under Lifted Map

Informal description

For any function $f : \alpha \to \beta$, the lifted map $\text{WithTop.map}\ f$ applied to the top element $\top$ of $\text{WithTop}\ \alpha$ returns the top element $\top$ of $\text{WithTop}\ \beta$.

WithTop.map_coe theorem

(f : α → β) (a : α) : map f a = f a

Full source

@[simp]
theorem map_coe (f : α → β) (a : α) : map f a = f a :=
  rfl

Lifted Map Preserves Function Application on Elements

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the lifted map $\text{WithTop.map}\ f$ applied to $a$ (viewed as an element of $\text{WithTop}\ \alpha$) equals $f(a)$.

WithTop.map_eq_top_iff theorem

{f : α → β} {a : WithTop α} : map f a = ⊤ ↔ a = ⊤

Full source

@[simp]
lemma map_eq_top_iff {f : α → β} {a : WithTop α} :
    mapmap f a = ⊤ ↔ a = ⊤ := Option.map_eq_none_iff

Top Element Characterization under Lifted Map

Informal description

For any function $f : \alpha \to \beta$ and any element $a$ in $\text{WithTop}\ \alpha$, the lifted map $\text{WithTop.map}\ f$ applied to $a$ equals the top element $\top$ if and only if $a$ itself is the top element $\top$.

WithTop.map_eq_some_iff theorem

{f : α → β} {y : β} {v : WithTop α} : WithTop.map f v = .some y ↔ ∃ x, v = .some x ∧ f x = y

Full source

theorem map_eq_some_iff {f : α → β} {y : β} {v : WithTop α} :
    WithTop.mapWithTop.map f v = .some y ↔ ∃ x, v = .some x ∧ f x = y := Option.map_eq_some_iff

Characterization of Lifted Map Output as Some Element

Informal description

For any function $f : \alpha \to \beta$, element $y \in \beta$, and element $v \in \text{WithTop}\ \alpha$, the lifted map $\text{WithTop.map}\ f$ applied to $v$ equals $\text{some}\ y$ if and only if there exists an element $x \in \alpha$ such that $v = \text{some}\ x$ and $f(x) = y$.

WithTop.some_eq_map_iff theorem

{f : α → β} {y : β} {v : WithTop α} : .some y = WithTop.map f v ↔ ∃ x, v = .some x ∧ f x = y

Full source

theorem some_eq_map_iff {f : α → β} {y : β} {v : WithTop α} :
    .some.some y = WithTop.map f v ↔ ∃ x, v = .some x ∧ f x = y := by
  cases v <;> simp [eq_comm]

Characterization of Preimage under Lifted Map in $\text{WithTop}$

Informal description

For any function $f : \alpha \to \beta$, element $y \in \beta$, and element $v \in \text{WithTop}\ \alpha$, the equality $\text{some}\ y = \text{WithTop.map}\ f\ v$ holds if and only if there exists an element $x \in \alpha$ such that $v = \text{some}\ x$ and $f(x) = y$.

WithTop.map_comm theorem

 {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
  map g₁ (map f₁ a) = map g₂ (map f₂ a)

Full source

theorem map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ}
    (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) : map g₁ (map f₁ a) = map g₂ (map f₂ a) :=
  Option.map_comm h _

Commutativity of Function Lifting in $\text{WithTop}$ under Composition

Informal description

For any functions $f_1: \alpha \to \beta$, $f_2: \alpha \to \gamma$, $g_1: \beta \to \delta$, and $g_2: \gamma \to \delta$ such that $g_1 \circ f_1 = g_2 \circ f_2$, and for any $a \in \alpha$, the following equality holds: $$ \text{map}\, g_1 (\text{map}\, f_1\, a) = \text{map}\, g_2 (\text{map}\, f_2\, a) $$ where $\text{map}$ denotes the lifting of a function to $\text{WithTop}$.

WithTop.map₂ definition

: (α → β → γ) → WithTop α → WithTop β → WithTop γ

Full source

/-- The image of a binary function `f : α → β → γ` as a function
`WithTop α → WithTop β → WithTop γ`.

Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
def map₂ : (α → β → γ) → WithTop α → WithTop β → WithTop γ := Option.map₂

Binary function on type extended with top element

Informal description

The function `WithTop.map₂` lifts a binary function $ f : \alpha \to \beta \to \gamma $ to operate on elements of `WithTop α` and `WithTop β`, returning `⊤` if either input is `⊤` and applying $ f $ to the values otherwise. Mathematically, this corresponds to the image of the function $ f $ viewed as a map $ \alpha \times \beta \to \gamma $.

WithTop.map₂_coe_coe theorem

(f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b

Full source

lemma map₂_coe_coe (f : α → β → γ) (a : α) (b : β) : map₂ f a b = f a b := rfl

Lifted Binary Function Evaluation on Non-Top Elements

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and elements $a \in \alpha$, $b \in \beta$, the lifted function `map₂` applied to $f$, $a$, and $b$ satisfies $\text{map₂}\, f\, a\, b = f\, a\, b$.

WithTop.map₂_top_left theorem

(f : α → β → γ) (b) : map₂ f ⊤ b = ⊤

Full source

@[simp] lemma map₂_top_left (f : α → β → γ) (b) : map₂ f ⊤ b = ⊤ := rfl

Top element preservation under `map₂` (left case)

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any element $b \in \text{WithTop}\ \beta$, the lifted binary operation satisfies $\text{map}_2\ f\ \top\ b = \top$.

WithTop.map₂_top_right theorem

(f : α → β → γ) (a) : map₂ f a ⊤ = ⊤

Full source

@[simp] lemma map₂_top_right (f : α → β → γ) (a) : map₂ f a ⊤ = ⊤ := by cases a <;> rfl

Top element preservation under `map₂` (right case)

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any element $a \in \text{WithTop}\ \alpha$, the lifted binary operation satisfies $\text{map}_2\ f\ a\ \top = \top$.

WithTop.map₂_coe_left theorem

(f : α → β → γ) (a : α) (b) : map₂ f a b = b.map fun b ↦ f a b

Full source

@[simp] lemma map₂_coe_left (f : α → β → γ) (a : α) (b) : map₂ f a b = b.map fun b ↦ f a b := rfl

Behavior of `map₂` on left coefficient in `WithTop`

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, element $a \in \alpha$, and element $b \in \text{WithTop}\ \beta$, the lifted binary operation satisfies: $$\text{map}_2\ f\ a\ b = \text{map}\ (\lambda b' \mapsto f\ a\ b')\ b$$ where $\text{map}$ applies the given function to the value inside $\text{WithTop}\ \beta$ if $b$ is not the top element $\top$, and returns $\top$ otherwise.

WithTop.map₂_coe_right theorem

(f : α → β → γ) (a) (b : β) : map₂ f a b = a.map (f · b)

Full source

@[simp] lemma map₂_coe_right (f : α → β → γ) (a) (b : β) : map₂ f a b = a.map (f · b) := by
  cases a <;> rfl

Behavior of `map₂` on right coefficient in `WithTop`

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \text{WithTop}\ \alpha$, and any element $b \in \beta$, the lifted binary operation satisfies: $$\text{map}_2\ f\ a\ b = \text{map}\ (\lambda a' \mapsto f\ a'\ b)\ a$$ where $\text{map}$ applies the given function to the value inside $\text{WithTop}\ \alpha$ if $a$ is not the top element $\top$, and returns $\top$ otherwise.

WithTop.map₂_eq_top_iff theorem

{f : α → β → γ} {a : WithTop α} {b : WithTop β} : map₂ f a b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Full source

@[simp] lemma map₂_eq_top_iff {f : α → β → γ} {a : WithTop α} {b : WithTop β} :
    map₂map₂ f a b = ⊤ ↔ a = ⊤ ∨ b = ⊤ := Option.map₂_eq_none_iff

Lifted Binary Operation Yields Top iff Either Argument is Top

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and elements $a \in \text{WithTop}\ \alpha$, $b \in \text{WithTop}\ \beta$, the lifted binary operation $\text{map}_2\ f\ a\ b$ yields the top element $\top$ if and only if either $a$ is $\top$ or $b$ is $\top$.

WithTop.map_toDual theorem

(f : αᵒᵈ → βᵒᵈ) (a : WithBot α) : map f (WithBot.toDual a) = a.map (toDual ∘ f)

Full source

theorem map_toDual (f : αᵒᵈ → βᵒᵈ) (a : WithBot α) :
    map f (WithBot.toDual a) = a.map (toDualtoDual ∘ f) :=
  rfl

Commutativity of `map` with `toDual` for `WithBot` and `WithTop`

Informal description

For any function $f : \alpha^\text{op} \to \beta^\text{op}$ and any element $a \in \text{WithBot}\ \alpha$, the following equality holds: $$\text{map}\ f\ (\text{WithBot.toDual}\ a) = \text{map}\ (\text{toDual} \circ f)\ a$$ where $\text{toDual}$ is the canonical map from $\alpha$ to $\alpha^\text{op}$ and $\text{map}$ lifts $f$ to operate on $\text{WithTop}\ \alpha^\text{op}$ and $\text{WithBot}\ \alpha$ respectively.

WithTop.map_ofDual theorem

(f : α → β) (a : WithBot αᵒᵈ) : map f (WithBot.ofDual a) = a.map (ofDual ∘ f)

Full source

theorem map_ofDual (f : α → β) (a : WithBot αᵒᵈ) : map f (WithBot.ofDual a) = a.map (ofDualofDual ∘ f) :=
  rfl

Compatibility of Map with Dualization in `WithBot` and `WithTop`

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \text{WithBot}\ \alpha^\text{op}$, the map of $f$ applied to the dual of $a$ is equal to the map of the composition of the dualization function with $f$ applied to $a$. In symbols: \[ \text{map}\ f\ (\text{WithBot.ofDual}\ a) = a.\text{map}\ (\text{ofDual} \circ f). \]

WithTop.toDual_map theorem

(f : α → β) (a : WithTop α) : WithTop.toDual (map f a) = WithBot.map (toDual ∘ f ∘ ofDual) (WithTop.toDual a)

Full source

theorem toDual_map (f : α → β) (a : WithTop α) :
    WithTop.toDual (map f a) = WithBot.map (toDualtoDual ∘ f ∘ ofDual) (WithTop.toDual a) :=
  rfl

Commutativity of $\text{WithTop.toDual}$ with Mapping Operations

Informal description

Let $f : \alpha \to \beta$ be a function and $a \in \text{WithTop}\ \alpha$. Then the equivalence $\text{WithTop.toDual}$ commutes with the mapping operations, satisfying: \[ \text{WithTop.toDual}(f(a)) = \text{WithBot.map}(\text{toDual} \circ f \circ \text{ofDual})(\text{WithTop.toDual}(a)) \] where: - $\text{WithTop.toDual} : \text{WithTop}\ \alpha \simeq \text{WithBot}\ \alpha^\text{op}$ is the canonical equivalence - $\text{toDual} : \alpha \to \alpha^\text{op}$ and $\text{ofDual} : \alpha^\text{op} \to \alpha$ are the duality operations - $f(a)$ denotes the lifted application of $f$ to $a$ in $\text{WithTop}\ \alpha$

WithTop.ofDual_map theorem

 (f : αᵒᵈ → βᵒᵈ) (a : WithTop αᵒᵈ) : WithTop.ofDual (map f a) = WithBot.map (ofDual ∘ f ∘ toDual) (WithTop.ofDual a)

Full source

theorem ofDual_map (f : αᵒᵈ → βᵒᵈ) (a : WithTop αᵒᵈ) :
    WithTop.ofDual (map f a) = WithBot.map (ofDualofDual ∘ f ∘ toDual) (WithTop.ofDual a) :=
  rfl

Compatibility of $\text{WithTop.ofDual}$ with Function Mapping

Informal description

Let $f : \alpha^\text{op} \to \beta^\text{op}$ be a function between order-dual types, and let $a$ be an element of $\text{WithTop}\ \alpha^\text{op}$. Then the equivalence $\text{WithTop.ofDual}$ satisfies: \[ \text{WithTop.ofDual} (\text{map}\ f\ a) = \text{WithBot.map} (\text{ofDual} \circ f \circ \text{toDual}) (\text{WithTop.ofDual}\ a) \] where $\text{map}$ denotes the lifting of $f$ to $\text{WithTop}\ \alpha^\text{op} \to \text{WithTop}\ \beta^\text{op}$ and $\text{WithBot.map}$ denotes the lifting of $\text{ofDual} \circ f \circ \text{toDual}$ to $\text{WithBot}\ \alpha \to \text{WithBot}\ \beta$.

WithTop.ne_top_iff_exists theorem

{x : WithTop α} : x ≠ ⊤ ↔ ∃ a : α, ↑a = x

Full source

lemma ne_top_iff_exists {x : WithTop α} : x ≠ ⊤x ≠ ⊤ ↔ ∃ a : α, ↑a = x := Option.ne_none_iff_exists

Characterization of Non-Top Elements in $\text{WithTop}\ \alpha$

Informal description

For any element $x$ in the type $\text{WithTop}\ \alpha$ (the extension of $\alpha$ with a top element $\top$), $x$ is not equal to $\top$ if and only if there exists an element $a \in \alpha$ such that the canonical injection of $a$ into $\text{WithTop}\ \alpha$ equals $x$.

WithTop.untop definition

: ∀ x : WithTop α, x ≠ ⊤ → α

Full source

/-- Deconstruct a `x : WithTop α` to the underlying value in `α`, given a proof that `x ≠ ⊤`. -/
def untop : ∀ x : WithTop α, x ≠ ⊤ → α | (x : α), _ => x

Underlying element of a non-top element in $\text{WithTop}\ \alpha$

Informal description

Given an element $x$ of type $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$) and a proof that $x \neq \top$, the function returns the underlying element of $\alpha$ corresponding to $x$.

WithTop.coe_untop theorem

: ∀ (x : WithTop α) hx, x.untop hx = x

Full source

@[simp] lemma coe_untop : ∀ (x : WithTop α) hx, x.untop hx = x | (x : α), _ => rfl

Underlying Element Equals Original in $\text{WithTop}\ \alpha$

Informal description

For any element $x$ of type $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$) and a proof $hx$ that $x \neq \top$, the underlying element obtained by applying the `untop` function to $x$ and $hx$ is equal to $x$ itself.

WithTop.canLift instance

: CanLift (WithTop α) α (↑) fun r => r ≠ ⊤

Full source

instance canLift : CanLift (WithTop α) α (↑) fun r => r ≠ ⊤ where
  prf x h := ⟨x.untop h, coe_untop _ _⟩

Lifting Condition for $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$, there is a canonical way to lift elements from $\alpha$ to $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$) via the injection function, with the condition that the lifted element is not equal to $\top$.

WithTop.instBot instance

[Bot α] : Bot (WithTop α)

Full source

instance instBot [Bot α] : Bot (WithTop α) where
  bot := (⊥ : α)

Bottom Element in $\text{WithTop}\ \alpha$ from Bottom Element in $\alpha$

Informal description

For any type $\alpha$ with a bottom element $\bot$, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element to $\alpha$) also has a bottom element, which is the image of $\bot$ under the canonical injection from $\alpha$ to $\text{WithTop}\ \alpha$.

WithTop.coe_bot theorem

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

Full source

@[simp, norm_cast] lemma coe_bot [Bot α] : ((⊥ : α) : WithTop α) = ⊥ := rfl

Bottom element injection in $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a bottom element $\bot$, the canonical injection of $\bot$ into $\text{WithTop}\ \alpha$ equals the bottom element of $\text{WithTop}\ \alpha$.

WithTop.coe_eq_bot theorem

[Bot α] {a : α} : (a : WithTop α) = ⊥ ↔ a = ⊥

Full source

@[simp, norm_cast] lemma coe_eq_bot [Bot α] {a : α} : (a : WithTop α) = ⊥ ↔ a = ⊥ := coe_eq_coe

Equivalence of Bottom Equality in $\text{WithTop}\ \alpha$ and $\alpha$

Informal description

For any type $\alpha$ with a bottom element $\bot$ and any element $a \in \alpha$, the equality $a = \bot$ holds in $\text{WithTop}\ \alpha$ if and only if $a = \bot$ holds in $\alpha$.

WithTop.bot_eq_coe theorem

[Bot α] {a : α} : (⊥ : WithTop α) = a ↔ ⊥ = a

Full source

@[simp, norm_cast] lemma bot_eq_coe [Bot α] {a : α} : (⊥ : WithTop α) = a ↔ ⊥ = a := coe_eq_coe

Equality of Bottom Element in $\text{WithTop}\ \alpha$ with Injected Element

Informal description

For any type $\alpha$ with a bottom element $\bot$ and any element $a \in \alpha$, the equality $\bot = a$ holds in $\text{WithTop}\ \alpha$ if and only if $\bot = a$ holds in $\alpha$.

WithTop.untop_eq_iff theorem

{a : WithTop α} {b : α} (h : a ≠ ⊤) : a.untop h = b ↔ a = b

Full source

theorem untop_eq_iff {a : WithTop α} {b : α} (h : a ≠ ⊤) :
    a.untop h = b ↔ a = b :=
  WithBot.unbot_eq_iff (α := αᵒᵈ) h

Equality of Underlying Value in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ in $\text{WithTop}\ \alpha$ that is not the top element (i.e., $a \neq \top$), and for any element $b$ in $\alpha$, the underlying value of $a$ in $\alpha$ (obtained via $\text{untop}$) is equal to $b$ if and only if $a$ is equal to $b$ (when viewed as an element of $\text{WithTop}\ \alpha$).

Equiv.withTopSubtypeNe definition

: { y : WithTop α // y ≠ ⊤ } ≃ α

Full source

/-- The equivalence between the non-top elements of `WithTop α` and `α`. -/
@[simps] def _root_.Equiv.withTopSubtypeNe : {y : WithTop α // y ≠ ⊤}{y : WithTop α // y ≠ ⊤} ≃ α where
  toFun := fun ⟨x,h⟩ => WithTop.untop x h
  invFun x := ⟨x, WithTop.coe_ne_top⟩
  left_inv _ := by simp
  right_inv _:= by simp

Equivalence between non-top elements of `WithTop α` and `α`

Informal description

The equivalence between the subtype of `WithTop α` consisting of elements that are not equal to the top element `⊤` and the original type `α`. The forward direction maps a pair `⟨x, h⟩` (where `x : WithTop α` and `h : x ≠ ⊤`) to the underlying element of `α` via `WithTop.untop`, while the inverse direction injects an element of `α` into `WithTop α` and proves it is not equal to `⊤`.

WithTop.le instance

: LE (WithTop α)

Full source

instance (priority := 10) le : LE (WithTop α) :=
  ⟨fun o₁ o₂ => ∀ a : α, o₂ = ↑a → ∃ b : α, o₁ = ↑b ∧ b ≤ a⟩

Partial Order Structure on `WithTop α`

Informal description

The type `WithTop α` is equipped with a canonical partial order structure, where the top element `⊤` is greater than all elements of `α`, and the order on `α` is inherited for elements in `α`.

WithTop.le_def theorem

: x ≤ y ↔ ∀ b : α, y = ↑b → ∃ a : α, x = ↑a ∧ a ≤ b

Full source

lemma le_def : x ≤ y ↔ ∀ b : α, y = ↑b → ∃ a : α, x = ↑a ∧ a ≤ b := .rfl

Characterization of Order in $\text{WithTop}\ \alpha$

Informal description

For elements $x, y$ in $\text{WithTop}\ \alpha$, the inequality $x \leq y$ holds if and only if for every $b \in \alpha$ such that $y = b$, there exists $a \in \alpha$ such that $x = a$ and $a \leq b$ in $\alpha$.

WithTop.coe_le_coe theorem

: (a : WithTop α) ≤ b ↔ a ≤ b

Full source

@[simp, norm_cast] lemma coe_le_coe : (a : WithTop α) ≤ b ↔ a ≤ b := by simp [le_def]

Order Preservation in $\text{WithTop}\ \alpha$ via Injection

Informal description

For any elements $a, b$ in $\alpha$, the inequality $(a : \text{WithTop}\ \alpha) \leq (b : \text{WithTop}\ \alpha)$ holds if and only if $a \leq b$ in $\alpha$.

WithTop.not_top_le_coe theorem

(a : α) : ¬⊤ ≤ (a : WithTop α)

Full source

lemma not_top_le_coe (a : α) : ¬ ⊤ ≤ (a : WithTop α) := by simp [le_def]

Top Element is Not Below Any Injected Element in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ in a type $\alpha$ with a partial order, the top element $\top$ in $\text{WithTop}\ \alpha$ is not less than or equal to the canonical injection of $a$ into $\text{WithTop}\ \alpha$, i.e., $\neg (\top \leq a)$.

WithTop.orderTop instance

: OrderTop (WithTop α)

Full source

instance orderTop : OrderTop (WithTop α) where le_top := by simp [le_def]

$\text{WithTop}\ \alpha$ has a top element

Informal description

For any type $\alpha$ with a partial order, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element to $\alpha$) has a greatest element $\top$ with respect to the inherited order.

WithTop.orderBot instance

[OrderBot α] : OrderBot (WithTop α)

Full source

instance orderBot [OrderBot α] : OrderBot (WithTop α) where bot_le x := by cases x <;> simp [le_def]

Bottom Element in $\text{WithTop}\ \alpha$ Inherited from $\alpha$

Informal description

For any type $\alpha$ with a partial order and a bottom element $\bot$, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element to $\alpha$) also has a bottom element, which is the image of $\bot$ under the canonical injection from $\alpha$ to $\text{WithTop}\ \alpha$, and this element is indeed the least element in the order on $\text{WithTop}\ \alpha$.

WithTop.boundedOrder instance

[OrderBot α] : BoundedOrder (WithTop α)

Full source

instance boundedOrder [OrderBot α] : BoundedOrder (WithTop α) :=
  { WithTop.orderTop, WithTop.orderBot with }

Bounded Order Structure on $\text{WithTop}\ \alpha$ Inherited from $\alpha$

Informal description

For any type $\alpha$ with a partial order and a bottom element $\bot$, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element to $\alpha$) is a bounded order, meaning it has both a greatest element $\top$ and a least element (the image of $\bot$ under the canonical injection from $\alpha$ to $\text{WithTop}\ \alpha$).

WithTop.top_le_iff theorem

: ∀ {a : WithTop α}, ⊤ ≤ a ↔ a = ⊤

Full source

/-- There is a general version `top_le_iff`, but this lemma does not require a `PartialOrder`. -/
@[simp]
protected theorem top_le_iff : ∀ {a : WithTop α}, ⊤⊤ ≤ a ↔ a = ⊤
  | (a : α) => by simp [not_top_le_coe _]
  | ⊤ => by simp

Characterization of Top Element in $\text{WithTop}\ \alpha$: $\top \leq a \leftrightarrow a = \top$

Informal description

For any element $a$ in the type $\text{WithTop}\ \alpha$, the top element $\top$ is less than or equal to $a$ if and only if $a$ is equal to $\top$.

WithTop.le_coe theorem

: ∀ {o : Option α}, a ∈ o → (@LE.le (WithTop α) _ o b ↔ a ≤ b)

Full source

theorem le_coe : ∀ {o : Option α}, a ∈ o → (@LE.le (WithTop α) _ o b ↔ a ≤ b)
  | _, rfl => coe_le_coe

Order Comparison in `WithTop α` via Injection

Informal description

For any element $a$ in the option type `Option α` (viewed as an element of `WithTop α`), and any element $b$ in $\alpha$, the inequality $a \leq b$ holds in `WithTop α` if and only if the corresponding inequality $a \leq b$ holds in $\alpha$.

WithTop.le_coe_iff theorem

: x ≤ b ↔ ∃ a : α, x = a ∧ a ≤ b

Full source

theorem le_coe_iff : x ≤ b ↔ ∃ a : α, x = a ∧ a ≤ b := by simp [le_def]

Characterization of Inequality in $\text{WithTop}\ \alpha$ via Injection

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ and any element $b$ in $\alpha$, the inequality $x \leq b$ holds if and only if there exists an element $a \in \alpha$ such that $x = a$ and $a \leq b$.

WithTop.coe_le_iff theorem

: ↑a ≤ x ↔ ∀ b : α, x = ↑b → a ≤ b

Full source

theorem coe_le_iff : ↑a ≤ x ↔ ∀ b : α, x = ↑b → a ≤ b := by simp [le_def]

Characterization of Inequality in $\text{WithTop}\ \alpha$ via Injection

Informal description

For an element $a$ of type $\alpha$ and an element $x$ of type $\text{WithTop}\ \alpha$, the inequality $\text{some}\ a \leq x$ holds if and only if for every $b \in \alpha$ such that $x = \text{some}\ b$, we have $a \leq b$.

IsMin.withTop theorem

(h : IsMin a) : IsMin (a : WithTop α)

Full source

protected theorem _root_.IsMin.withTop (h : IsMin a) : IsMin (a : WithTop α) :=
  fun x ↦ by cases x <;> simp; simpa using @h _

Minimality Preservation in $\text{WithTop}\ \alpha$

Informal description

If an element $a$ of a type $\alpha$ with a preorder is minimal in $\alpha$, then its image under the canonical injection into $\text{WithTop}\ \alpha$ is also minimal in $\text{WithTop}\ \alpha$.

WithTop.untop_le_iff theorem

(hx : x ≠ ⊤) : untop x hx ≤ b ↔ x ≤ b

Full source

lemma untop_le_iff (hx : x ≠ ⊤) : untopuntop x hx ≤ b ↔ x ≤ b := by lift x to α using id hx; simp

Inequality Characterization for Untop in $\text{WithTop}\ \alpha$

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ such that $x \neq \top$, and for any element $b$ in $\alpha$, the inequality $\text{untop}(x, hx) \leq b$ holds if and only if $x \leq b$, where $\text{untop}(x, hx)$ is the underlying element of $\alpha$ corresponding to $x$.

WithTop.le_untop_iff theorem

(hy : y ≠ ⊤) : a ≤ untop y hy ↔ a ≤ y

Full source

lemma le_untop_iff (hy : y ≠ ⊤) : a ≤ untop y hy ↔ a ≤ y := by lift y to α using id hy; simp

Inequality Characterization for Non-Top Elements in $\text{WithTop}\ \alpha$

Informal description

For any element $y$ in $\text{WithTop}\ \alpha$ such that $y \neq \top$, and for any element $a$ in $\alpha$, the inequality $a \leq \text{untop}(y, hy)$ holds if and only if $a \leq y$, where $\text{untop}(y, hy)$ is the underlying element of $\alpha$ corresponding to $y$.

WithTop.le_untopD_iff theorem

(hy : y = ⊤ → a ≤ b) : a ≤ y.untopD b ↔ a ≤ y

Full source

lemma le_untopD_iff (hy : y = ⊤ → a ≤ b) : a ≤ y.untopD b ↔ a ≤ y := by cases y <;> simp [hy]

Inequality Characterization for $\text{untopD}$ in $\text{WithTop}\ \alpha$

Informal description

Let $\alpha$ be a type with a partial order, and let $a, b \in \alpha$. For any element $y$ in $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$), if $y = \top$ implies $a \leq b$, then the inequality $a \leq \text{untopD}(y, b)$ holds if and only if $a \leq y$. Here, $\text{untopD}(y, b)$ is defined as $b$ when $y = \top$, and as the underlying element of $\alpha$ when $y \neq \top$.

WithTop.lt instance

: LT (WithTop α)

Full source

instance (priority := 10) lt : LT (WithTop α) :=
  ⟨fun o₁ o₂ : Option α => ∃ b ∈ o₁, ∀ a ∈ o₂, b < a⟩

Order on $\alpha$ Extended with a Top Element

Informal description

For any type $\alpha$ with an order, the type `WithTop α` (which is $\alpha$ extended with a top element $\top$) has a canonical less-than relation defined by lifting the order from $\alpha$ and setting $\top$ to be greater than all elements of $\alpha$.

WithTop.lt_def theorem

: x < y ↔ ∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b

Full source

lemma lt_def : x < y ↔ ∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b := .rfl

Characterization of Order Relation in $\text{WithTop}\ \alpha$

Informal description

For elements $x$ and $y$ in $\text{WithTop}\ \alpha$ (where $\alpha$ is an ordered type extended with a top element $\top$), the relation $x < y$ holds if and only if there exists an element $a \in \alpha$ such that $x$ is the injection of $a$ into $\text{WithTop}\ \alpha$ (i.e., $x = \text{some}\ a$) and for every element $b \in \alpha$, if $y$ is the injection of $b$ (i.e., $y = \text{some}\ b$), then $a < b$ in $\alpha$.

WithTop.coe_lt_coe theorem

: (a : WithTop α) < b ↔ a < b

Full source

@[simp, norm_cast] lemma coe_lt_coe : (a : WithTop α) < b ↔ a < b := by simp [lt_def]

Inequality Preservation in $\text{WithTop}\ \alpha$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the inequality $a < b$ holds in $\text{WithTop}\ \alpha$ if and only if $a < b$ holds in $\alpha$.

WithTop.coe_lt_top theorem

(a : α) : (a : WithTop α) < ⊤

Full source

@[simp] lemma coe_lt_top (a : α) : (a : WithTop α) < ⊤ := by simp [lt_def]

Injected Elements are Below Top in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ of type $\alpha$, the injection of $a$ into $\text{WithTop}\ \alpha$ (denoted as $\text{some}\ a$) is strictly less than the top element $\top$.

WithTop.not_top_lt theorem

(a : WithTop α) : ¬⊤ < a

Full source

@[simp] protected lemma not_top_lt (a : WithTop α) : ¬⊤ < a := by simp [lt_def]

Top Element is Not Less Than Any Element in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ in the type $\alpha$ extended with a top element $\top$, the top element is not less than $a$, i.e., $\neg (\top < a)$.

WithTop.lt_iff_exists_coe theorem

: x < y ↔ ∃ a : α, x = a ∧ a < y

Full source

lemma lt_iff_exists_coe : x < y ↔ ∃ a : α, x = a ∧ a < y := by cases x <;> simp

Characterization of Inequality in $\text{WithTop}\ \alpha$ via Underlying Element

Informal description

For any elements $x, y$ in $\text{WithTop}\ \alpha$, the inequality $x < y$ holds if and only if there exists an element $a \in \alpha$ such that $x = a$ (i.e., $x$ is the injection of $a$ into $\text{WithTop}\ \alpha$) and $a < y$ in the order on $\alpha$.

WithTop.coe_lt_iff theorem

: a < y ↔ ∀ b : α, y = b → a < b

Full source

lemma coe_lt_iff : a < y ↔ ∀ b : α, y = b → a < b := by simp [lt_def]

Characterization of Inequality in $\text{WithTop}\ \alpha$ via Underlying Order

Informal description

For an element $a$ in $\alpha$ and an element $y$ in $\text{WithTop}\ \alpha$, the inequality $a < y$ holds if and only if for every $b \in \alpha$ such that $y = b$, we have $a < b$.

WithTop.lt_top_iff_ne_top theorem

: x < ⊤ ↔ x ≠ ⊤

Full source

/-- A version of `lt_top_iff_ne_top` for `WithTop` that only requires `LT α`, not
`PartialOrder α`. -/
protected lemma lt_top_iff_ne_top : x < ⊤ ↔ x ≠ ⊤ := by cases x <;> simp

Characterization of Elements Less Than Top in $\text{WithTop}\ \alpha$

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$, the inequality $x < \top$ holds if and only if $x$ is not equal to the top element $\top$.

WithTop.lt_untop_iff theorem

(hy : y ≠ ⊤) : a < y.untop hy ↔ a < y

Full source

lemma lt_untop_iff (hy : y ≠ ⊤) : a < y.untop hy ↔ a < y := by lift y to α using id hy; simp

Inequality Preservation Under Untop in $\text{WithTop}\ \alpha$

Informal description

For any element $y$ in $\text{WithTop}\ \alpha$ such that $y \neq \top$, and for any element $a$ in $\alpha$, the inequality $a < \text{untop}(y, hy)$ holds if and only if $a < y$, where $\text{untop}(y, hy)$ is the underlying element of $y$ in $\alpha$ given the proof $hy$ that $y \neq \top$.

WithTop.untop_lt_iff theorem

(hx : x ≠ ⊤) : x.untop hx < b ↔ x < b

Full source

lemma untop_lt_iff (hx : x ≠ ⊤) : x.untop hx < b ↔ x < b := by lift x to α using id hx; simp

Comparison of Extracted Element in $\text{WithTop}\ \alpha$: $x.\text{untop}\ hx < b \leftrightarrow x < b$

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ such that $x \neq \top$, and any element $b$ in $\alpha$, the inequality $x.\text{untop}\ hx < b$ holds if and only if $x < b$.

WithTop.lt_untopD_iff theorem

(hy : y = ⊤ → a < b) : a < y.untopD b ↔ a < y

Full source

lemma lt_untopD_iff (hy : y = ⊤ → a < b) : a < y.untopD b ↔ a < y := by cases y <;> simp [hy]

Comparison with Default Extraction in $\text{WithTop}\ \alpha$: $a < \text{untopD}(y, b) \leftrightarrow a < y$

Informal description

Let $a$ and $b$ be elements of a type $\alpha$ with an order, and let $y$ be an element of $\alpha$ extended with a top element $\top$ (i.e., $y \in \text{WithTop}\ \alpha$). Given the implication that if $y = \top$ then $a < b$, the following equivalence holds: \[ a < \text{untopD}(y, b) \leftrightarrow a < y, \] where $\text{untopD}(y, b)$ is the default value extraction function that returns $b$ if $y = \top$ and the underlying value of $y$ otherwise.

WithTop.preorder instance

[Preorder α] : Preorder (WithTop α)

Full source

instance preorder [Preorder α] : Preorder (WithTop α) where
  lt_iff_le_not_le x y := by cases x <;> cases y <;> simp [lt_iff_le_not_le]
  le_refl x := by cases x <;> simp [le_def]
  le_trans x y z := by cases x <;> cases y <;> cases z <;> simp [le_def]; simpa using le_trans

Preorder Structure on $\alpha$ Extended with a Top Element

Informal description

For any type $\alpha$ with a preorder, the type `WithTop α` (which is $\alpha$ extended with a top element $\top$) has a canonical preorder structure that extends the preorder on $\alpha$ by making $\top$ the greatest element.

WithTop.partialOrder instance

[PartialOrder α] : PartialOrder (WithTop α)

Full source

instance partialOrder [PartialOrder α] : PartialOrder (WithTop α) where
  le_antisymm x y := by cases x <;> cases y <;> simp [le_def]; simpa using le_antisymm

Partial Order Structure on $\alpha$ Extended with a Top Element

Informal description

For any type $\alpha$ with a partial order, the type $\text{WithTop}\ \alpha$ (which is $\alpha$ extended with a top element $\top$) has a canonical partial order structure that extends the partial order on $\alpha$ by making $\top$ the greatest element.

WithTop.coe_strictMono theorem

: StrictMono (fun a : α => (a : WithTop α))

Full source

theorem coe_strictMono : StrictMono (fun a : α => (a : WithTop α)) := fun _ _ => coe_lt_coe.2

Strict Monotonicity of the Injection into $\text{WithTop}\ \alpha$

Informal description

The canonical injection map $a \mapsto \text{some}\ a$ from a type $\alpha$ to $\text{WithTop}\ \alpha$ is strictly monotone. That is, for any $a, b \in \alpha$, if $a < b$ in $\alpha$, then $(a : \text{WithTop}\ \alpha) < (b : \text{WithTop}\ \alpha)$.

WithTop.coe_mono theorem

: Monotone (fun a : α => (a : WithTop α))

Full source

theorem coe_mono : Monotone (fun a : α => (a : WithTop α)) := fun _ _ => coe_le_coe.2

Monotonicity of the Injection into $\text{WithTop}\ \alpha$

Informal description

The canonical injection from a type $\alpha$ to $\text{WithTop}\ \alpha$, given by $a \mapsto \text{some}\ a$, is monotone. That is, for any $a, b \in \alpha$, if $a \leq b$ in $\alpha$, then $(a : \text{WithTop}\ \alpha) \leq (b : \text{WithTop}\ \alpha)$.

WithTop.monotone_iff theorem

{f : WithTop α → β} : Monotone f ↔ Monotone (fun (a : α) => f a) ∧ ∀ x : α, f x ≤ f ⊤

Full source

theorem monotone_iff {f : WithTop α → β} :
    MonotoneMonotone f ↔ Monotone (fun (a : α) => f a) ∧ ∀ x : α, f x ≤ f ⊤ :=
  ⟨fun h => ⟨h.comp WithTop.coe_mono, fun _ => h le_top⟩, fun h =>
    WithTop.forall.2
      ⟨WithTop.forall.2 ⟨fun _ => le_rfl, fun _ h => (not_top_le_coe _ h).elim⟩, fun x =>
        WithTop.forall.2 ⟨fun _ => h.2 x, fun _ hle => h.1 (coe_le_coe.1 hle)⟩⟩⟩

Characterization of Monotone Functions on $\text{WithTop}\ \alpha$

Informal description

A function $f : \text{WithTop}\ \alpha \to \beta$ is monotone if and only if its restriction to $\alpha$ is monotone and for every $x \in \alpha$, $f(x) \leq f(\top)$.

WithTop.monotone_map_iff theorem

{f : α → β} : Monotone (WithTop.map f) ↔ Monotone f

Full source

@[simp]
theorem monotone_map_iff {f : α → β} : MonotoneMonotone (WithTop.map f) ↔ Monotone f :=
  monotone_iff.trans <| by simp [Monotone]

Monotonicity of Lifted Map to $\text{WithTop}$ iff Original Map is Monotone

Informal description

For any function $f : \alpha \to \beta$, the lifted map $\text{WithTop.map}\ f : \text{WithTop}\ \alpha \to \text{WithTop}\ \beta$ is monotone if and only if $f$ is monotone.

WithTop.strictMono_iff theorem

{f : WithTop α → β} : StrictMono f ↔ StrictMono (fun (a : α) => f a) ∧ ∀ x : α, f x < f ⊤

Full source

theorem strictMono_iff {f : WithTop α → β} :
    StrictMonoStrictMono f ↔ StrictMono (fun (a : α) => f a) ∧ ∀ x : α, f x < f ⊤ :=
  ⟨fun h => ⟨h.comp WithTop.coe_strictMono, fun _ => h (coe_lt_top _)⟩, fun h =>
    WithTop.forall.2
      ⟨WithTop.forall.2 ⟨flip absurd (lt_irrefl _), fun _ h => (not_top_lt h).elim⟩, fun x =>
        WithTop.forall.2 ⟨fun _ => h.2 x, fun _ hle => h.1 (coe_lt_coe.1 hle)⟩⟩⟩

Characterization of Strictly Monotone Functions on $\alpha$ Extended with Top

Informal description

A function $f : \text{WithTop}\ \alpha \to \beta$ is strictly monotone if and only if its restriction to $\alpha$ is strictly monotone and for every $x \in \alpha$, $f(x) < f(\top)$.

WithTop.strictAnti_iff theorem

{f : WithTop α → β} : StrictAnti f ↔ StrictAnti (fun a ↦ f a : α → β) ∧ ∀ x : α, f ⊤ < f x

Full source

theorem strictAnti_iff {f : WithTop α → β} :
    StrictAntiStrictAnti f ↔ StrictAnti (fun a ↦ f a : α → β) ∧ ∀ x : α, f ⊤ < f x :=
  strictMono_iff (β := βᵒᵈ)

Characterization of Strictly Antitone Functions on $\alpha$ Extended with Top

Informal description

A function $f : \text{WithTop}\ \alpha \to \beta$ is strictly antitone if and only if its restriction to $\alpha$ is strictly antitone and for every $x \in \alpha$, $f(\top) < f(x)$.

WithTop.strictMono_map_iff theorem

{f : α → β} : StrictMono (WithTop.map f) ↔ StrictMono f

Full source

@[simp]
theorem strictMono_map_iff {f : α → β} : StrictMonoStrictMono (WithTop.map f) ↔ StrictMono f :=
  strictMono_iff.trans <| by simp [StrictMono, coe_lt_top]

Strict Monotonicity of Lifted Map on Extended Type $\leftrightarrow$ Strict Monotonicity of Original Function

Informal description

For any function $f : \alpha \to \beta$, the lifted map $\text{WithTop.map}\ f : \text{WithTop}\ \alpha \to \text{WithTop}\ \beta$ is strictly monotone if and only if $f$ is strictly monotone.

WithTop.map_le_iff theorem

(f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) : x.map f ≤ y.map f ↔ x ≤ y

Full source

theorem map_le_iff (f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
    x.map f ≤ y.map f ↔ x ≤ y := by cases x <;> cases y <;> simp [mono_iff]

Order-Preserving Property of Lifted Maps on Extended Types: $\text{map}\ f\ x \leq \text{map}\ f\ y \leftrightarrow x \leq y$

Informal description

Let $f : \alpha \to \beta$ be a function between partially ordered types, and suppose that for all $a, b \in \alpha$, $f(a) \leq f(b)$ if and only if $a \leq b$. Then for any $x, y \in \text{WithTop}\ \alpha$, the inequality $\text{map}\ f\ x \leq \text{map}\ f\ y$ holds if and only if $x \leq y$.

WithTop.coe_untopD_le theorem

(y : WithTop α) (a : α) : y.untopD a ≤ y

Full source

theorem coe_untopD_le (y : WithTop α) (a : α) : y.untopD a ≤ y :=  by cases y <;> simp

Default Extraction Preserves Order in $\text{WithTop}\ \alpha$

Informal description

For any element $y$ in $\text{WithTop}\ \alpha$ and any default value $a \in \alpha$, the value obtained by applying the default extraction function $\text{untopD}$ to $y$ with default $a$ is less than or equal to $y$ in the order of $\text{WithTop}\ \alpha$.

WithTop.coe_top_lt theorem

[OrderTop α] : (⊤ : α) < x ↔ x = ⊤

Full source

@[simp]
theorem coe_top_lt [OrderTop α] : (⊤ : α) < x ↔ x = ⊤ := by cases x <;> simp

Top Element Inequality in Extended Type: $\top < x \leftrightarrow x = \top$

Informal description

For any type $\alpha$ with an order and a top element $\top$, the inequality $\top < x$ holds in $\text{WithTop}\ \alpha$ if and only if $x$ is equal to $\top$.

WithTop.forall_coe_le_iff_le theorem

[NoTopOrder α] : (∀ a : α, a ≤ x → a ≤ y) ↔ x ≤ y

Full source

lemma forall_coe_le_iff_le [NoTopOrder α] : (∀ a : α, a ≤ x → a ≤ y) ↔ x ≤ y :=
  WithBot.forall_le_coe_iff_le (α := αᵒᵈ)

Characterization of Order Relation in $\text{WithTop }\alpha$ via Universal Property

Informal description

Let $\alpha$ be a type with a preorder and no top element. For any elements $x, y \in \text{WithTop }\alpha$, the following are equivalent: 1. For every $a \in \alpha$, if $a \leq x$ then $a \leq y$. 2. $x \leq y$. Here, $\text{WithTop }\alpha$ denotes the type $\alpha$ extended with a top element $\top$, and the order is extended such that $x \leq \top$ for all $x \in \text{WithTop }\alpha$.

WithTop.semilatticeInf instance

[SemilatticeInf α] : SemilatticeInf (WithTop α)

Full source

instance semilatticeInf [SemilatticeInf α] : SemilatticeInf (WithTop α) where
  inf
    -- note this is `Option.merge`, but with the right defeq when unfolding
    | ⊤, ⊤ => ⊤
    | (a : α), ⊤ => a
    | ⊤, (b : α) => b
    | (a : α), (b : α) => ↑(a ⊓ b)
  inf_le_left x y := by cases x <;> cases y <;> simp
  inf_le_right x y := by cases x <;> cases y <;> simp
  le_inf x y z := by cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

Meet-Semilattice Structure on $\alpha$ Extended with a Top Element

Informal description

For any meet-semilattice $\alpha$, the type $\alpha$ extended with a top element $\top$ forms a meet-semilattice, where the meet operation is extended in the natural way: the meet of $\top$ with any element $a$ is $a$, and the meet of two elements from $\alpha$ is their meet in $\alpha$.

WithTop.coe_inf theorem

[SemilatticeInf α] (a b : α) : ((a ⊓ b : α) : WithTop α) = (a : WithTop α) ⊓ b

Full source

theorem coe_inf [SemilatticeInf α] (a b : α) : ((a ⊓ b : α) : WithTop α) = (a : WithTop α) ⊓ b :=
  rfl

Preservation of Meet under Injection into $\text{WithTop}\ \alpha$

Informal description

Let $\alpha$ be a meet-semilattice. For any two elements $a, b \in \alpha$, the canonical injection of their meet $a \sqcap b$ into $\text{WithTop}\ \alpha$ is equal to the meet of their injections, i.e., $(a \sqcap b : \text{WithTop}\ \alpha) = (a : \text{WithTop}\ \alpha) \sqcap b$.

WithTop.semilatticeSup instance

[SemilatticeSup α] : SemilatticeSup (WithTop α)

Full source

instance semilatticeSup [SemilatticeSup α] : SemilatticeSup (WithTop α) where
  sup := .map₂ (· ⊔ ·)
  le_sup_left x y := by cases x <;> cases y <;> simp
  le_sup_right x y := by cases x <;> cases y <;> simp
  sup_le x y z := by cases x <;> cases y <;> cases z <;> simp; simpa using sup_le

Join-Semilattice Structure on $\alpha$ Extended with a Top Element

Informal description

For any join-semilattice $\alpha$, the type $\text{WithTop}\ \alpha$ (which is $\alpha$ extended with a top element $\top$) has a canonical join-semilattice structure that extends the join-semilattice structure on $\alpha$ by making $\top$ the greatest element and preserving the supremum operation.

WithTop.coe_sup theorem

[SemilatticeSup α] (a b : α) : ((a ⊔ b : α) : WithTop α) = (a : WithTop α) ⊔ b

Full source

theorem coe_sup [SemilatticeSup α] (a b : α) : ((a ⊔ b : α) : WithTop α) = (a : WithTop α) ⊔ b :=
  rfl

Supremum Preservation in $\text{WithTop}\ \alpha$

Informal description

For any join-semilattice $\alpha$ and elements $a, b \in \alpha$, the canonical injection of the supremum $a \sqcup b$ into $\text{WithTop}\ \alpha$ is equal to the supremum of the injections of $a$ and $b$ in $\text{WithTop}\ \alpha$. That is, $(a \sqcup b : \text{WithTop}\ \alpha) = (a : \text{WithTop}\ \alpha) \sqcup (b : \text{WithTop}\ \alpha)$.

WithTop.lattice instance

[Lattice α] : Lattice (WithTop α)

Full source

instance lattice [Lattice α] : Lattice (WithTop α) :=
  { WithTop.semilatticeSup, WithTop.semilatticeInf with }

Lattice Structure on $\alpha$ Extended with a Top Element

Informal description

For any lattice $\alpha$, the type $\alpha$ extended with a top element $\top$ forms a lattice, where the join and meet operations are extended in the natural way: the join (resp. meet) of $\top$ with any element $a$ is $\top$ (resp. $a$), and the join and meet of two elements from $\alpha$ are their join and meet in $\alpha$.

WithTop.distribLattice instance

[DistribLattice α] : DistribLattice (WithTop α)

Full source

instance distribLattice [DistribLattice α] : DistribLattice (WithTop α) where
  le_sup_inf x y z := by
    cases x <;> cases y <;> cases z <;> simp [← coe_inf, ← coe_sup]
    simpa [← coe_inf, ← coe_sup] using le_sup_inf

Distributive Lattice Structure on $\alpha$ Extended with a Top Element

Informal description

For any distributive lattice $\alpha$, the type $\alpha$ extended with a top element $\top$ forms a distributive lattice, where the join and meet operations are extended in the natural way: the join (resp. meet) of $\top$ with any element $a$ is $\top$ (resp. $a$), and the join and meet of two elements from $\alpha$ are their join and meet in $\alpha$.

WithTop.decidableEq instance

[DecidableEq α] : DecidableEq (WithTop α)

Full source

instance decidableEq [DecidableEq α] : DecidableEq (WithTop α) :=
  inferInstanceAs <| DecidableEq (Option α)

Decidable Equality for $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a decidable equality, the type $\text{WithTop}\ \alpha$ (obtained by adjoining a top element to $\alpha$) also has decidable equality.

WithTop.decidableLE instance

[LE α] [DecidableLE α] : DecidableLE (WithTop α)

Full source

instance decidableLE [LE α] [DecidableLE α] : DecidableLE (WithTop α)
  | _, ⊤ => isTrue <| by simp
  | ⊤, (a : α) => isFalse <| by simp
  | (a : α), (b : α) => decidable_of_iff' _ coe_le_coe

Decidable Less-Than-or-Equal Relation on $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a decidable less-than-or-equal-to relation, the type $\text{WithTop}\ \alpha$ (obtained by adjoining a top element to $\alpha$) also has a decidable less-than-or-equal-to relation.

WithTop.decidableLT instance

[LT α] [DecidableLT α] : DecidableLT (WithTop α)

Full source

instance decidableLT [LT α] [DecidableLT α] : DecidableLT (WithTop α)
  | ⊤, _ => isFalse <| by simp
  | (a : α), ⊤ => isTrue <| by simp
  | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe

Decidable Less-Than Relation on $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a decidable less-than relation, the type $\text{WithTop}\ \alpha$ (obtained by adjoining a top element to $\alpha$) also has a decidable less-than relation.

WithTop.isTotal_le instance

[LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithTop α) (· ≤ ·)

Full source

instance isTotal_le [LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithTop α) (· ≤ ·) where
  total x y := by cases x <;> cases y <;> simp; simpa using IsTotal.total ..

Total Order on $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a total order $\leq$, the order on $\text{WithTop}\ \alpha$ (obtained by adjoining a top element to $\alpha$) is also total.

WithTop.linearOrder instance

[LinearOrder α] : LinearOrder (WithTop α)

Full source

instance linearOrder [LinearOrder α] : LinearOrder (WithTop α) := Lattice.toLinearOrder _

Linear Order on $\alpha$ Extended with a Top Element

Informal description

For any linearly ordered set $\alpha$, the type $\alpha$ extended with a top element $\top$ forms a linear order, where the order is extended by declaring $\top$ to be greater than all elements of $\alpha$.

WithTop.coe_min theorem

(a b : α) : ↑(min a b) = min (a : WithTop α) b

Full source

@[simp, norm_cast] lemma coe_min (a b : α) : ↑(min a b) = min (a : WithTop α) b := rfl

Minimum Operation Commutes with Injection into $\text{WithTop}\ \alpha$

Informal description

For any two elements $a$ and $b$ in a type $\alpha$, the canonical injection of their minimum $\min(a, b)$ into $\text{WithTop}\ \alpha$ is equal to the minimum of their injections $a$ and $b$ in $\text{WithTop}\ \alpha$. In symbols: $$ \uparrow(\min(a, b)) = \min(\uparrow a, \uparrow b) $$

WithTop.coe_max theorem

(a b : α) : ↑(max a b) = max (a : WithTop α) b

Full source

@[simp, norm_cast] lemma coe_max (a b : α) : ↑(max a b) = max (a : WithTop α) b := rfl

Preservation of Maximum under Injection into $\text{WithTop}\ \alpha$

Informal description

For any two elements $a$ and $b$ in a type $\alpha$, the image of their maximum under the canonical injection into $\text{WithTop}\ \alpha$ (i.e., $\text{some}(\max(a, b))$) equals the maximum of their images in $\text{WithTop}\ \alpha$ (i.e., $\max(\text{some}(a), \text{some}(b))$).

WithTop.le_of_forall_lt_iff_le theorem

: (∀ b : α, x < b → y ≤ b) ↔ y ≤ x

Full source

lemma le_of_forall_lt_iff_le : (∀ b : α, x < b → y ≤ b) ↔ y ≤ x := by
  cases x <;> cases y <;> simp [exists_gt, forall_gt_imp_ge_iff_le_of_dense]

Characterization of Order Relation in $\text{WithTop}\ \alpha$ via Strict Inequality

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ and any element $y$ in $\text{WithTop}\ \alpha$, the following are equivalent: 1. For every element $b$ in $\alpha$, if $x < b$ then $y \leq b$. 2. $y \leq x$.

WithTop.ge_of_forall_gt_iff_ge theorem

: (∀ a : α, a < x → a ≤ y) ↔ x ≤ y

Full source

lemma ge_of_forall_gt_iff_ge : (∀ a : α, a < x → a ≤ y) ↔ x ≤ y := by
  cases x <;> cases y <;> simp [exists_gt, forall_lt_imp_le_iff_le_of_dense]

Characterization of Order Relation in $\text{WithTop}\ \alpha$ via Strict Inequality (Dual Version)

Informal description

For any elements $x, y$ in $\text{WithTop}\ \alpha$, the following are equivalent: 1. For every $a \in \alpha$, if $a < x$ then $a \leq y$. 2. $x \leq y$.

WithTop.instWellFoundedLT instance

[LT α] [WellFoundedLT α] : WellFoundedLT (WithTop α)

Full source

instance instWellFoundedLT [LT α] [WellFoundedLT α] : WellFoundedLT (WithTop α) :=
  inferInstanceAs <| WellFoundedLT (WithBot αᵒᵈ)ᵒᵈ

Well-Founded Less-Than Relation on $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a well-founded less-than relation, the type $\text{WithTop}\ \alpha$ (which is $\alpha$ extended with a top element $\top$) also has a well-founded less-than relation.

WithTop.instWellFoundedGT instance

[LT α] [WellFoundedGT α] : WellFoundedGT (WithTop α)

Full source

instance instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithTop α) :=
  inferInstanceAs <| WellFoundedGT (WithBot αᵒᵈ)ᵒᵈ

Well-Founded Greater-Than Relation on $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ with a well-founded greater-than relation, the type $\text{WithTop}\ \alpha$ (which is $\alpha$ extended with a top element $\top$) also has a well-founded greater-than relation.

WithTop.trichotomous.lt instance

[Preorder α] [IsTrichotomous α (· < ·)] : IsTrichotomous (WithTop α) (· < ·)

Full source

instance trichotomous.lt [Preorder α] [IsTrichotomous α (· < ·)] :
    IsTrichotomous (WithTop α) (· < ·) where
  trichotomous x y := by cases x <;> cases y <;> simp [trichotomous]

Trichotomy of Strict Order on $\text{WithTop}\ \alpha$

Informal description

For any preorder $\alpha$ with a trichotomous strict order relation $<$, the extended type $\text{WithTop}\ \alpha$ (obtained by adding a top element $\top$ to $\alpha$) also has a trichotomous strict order relation $<$. This means that for any two elements $x, y \in \text{WithTop}\ \alpha$, exactly one of the following holds: $x < y$, $x = y$, or $y < x$.

WithTop.IsWellOrder.lt instance

[Preorder α] [IsWellOrder α (· < ·)] : IsWellOrder (WithTop α) (· < ·)

Full source

instance IsWellOrder.lt [Preorder α] [IsWellOrder α (· < ·)] : IsWellOrder (WithTop α) (· < ·) where

Well-Founded Strict Order on $\alpha$ Extended with a Top Element

Informal description

For any preorder $\alpha$ with a well-founded strict order relation $<$, the extended type $\text{WithTop}\ \alpha$ (obtained by adding a top element $\top$ to $\alpha$) also has a well-founded strict order relation $<$.

WithTop.trichotomous.gt instance

[Preorder α] [IsTrichotomous α (· > ·)] : IsTrichotomous (WithTop α) (· > ·)

Full source

instance trichotomous.gt [Preorder α] [IsTrichotomous α (· > ·)] :
    IsTrichotomous (WithTop α) (· > ·) :=
  have : IsTrichotomous α (· < ·) := .swap _; .swap _

Trichotomy of Strict Greater-Than Order on $\alpha$ Extended with a Top Element

Informal description

For any preorder $\alpha$ with a trichotomous strict order relation $>$, the extended type $\text{WithTop}\ \alpha$ (obtained by adding a top element $\top$ to $\alpha$) also has a trichotomous strict order relation $>$. This means that for any two elements $x, y \in \text{WithTop}\ \alpha$, exactly one of the following holds: $x > y$, $x = y$, or $y > x$.

WithTop.IsWellOrder.gt instance

[Preorder α] [IsWellOrder α (· > ·)] : IsWellOrder (WithTop α) (· > ·)

Full source

instance IsWellOrder.gt [Preorder α] [IsWellOrder α (· > ·)] : IsWellOrder (WithTop α) (· > ·) where

Well-Founded Strict Greater-Than Order on $\alpha$ Extended with a Top Element

Informal description

For any preorder $\alpha$ with a well-founded strict greater-than relation $>$, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element $\top$ to $\alpha$) also has a well-founded strict greater-than relation $>$.

WithBot.trichotomous.lt instance

[Preorder α] [h : IsTrichotomous α (· < ·)] : IsTrichotomous (WithBot α) (· < ·)

Full source

instance _root_.WithBot.trichotomous.lt [Preorder α] [h : IsTrichotomous α (· < ·)] :
    IsTrichotomous (WithBot α) (· < ·) where
  trichotomous x y := by cases x <;> cases y <;> simp [trichotomous]

Trichotomy of Strict Order on $\alpha$ with Bottom Element

Informal description

For any preorder $\alpha$ with a trichotomous strict order relation $<$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) also has a trichotomous strict order relation $<$.

WithBot.isWellOrder.lt instance

[Preorder α] [IsWellOrder α (· < ·)] : IsWellOrder (WithBot α) (· < ·)

Full source

instance _root_.WithBot.isWellOrder.lt [Preorder α] [IsWellOrder α (· < ·)] :
    IsWellOrder (WithBot α) (· < ·) where

Well-Founded Strict Order on $\alpha$ with Bottom Element

Informal description

For any preorder $\alpha$ with a well-founded strict order relation $<$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) also has a well-founded strict order relation $<$.

WithBot.trichotomous.gt instance

[Preorder α] [h : IsTrichotomous α (· > ·)] : IsTrichotomous (WithBot α) (· > ·)

Full source

instance _root_.WithBot.trichotomous.gt [Preorder α] [h : IsTrichotomous α (· > ·)] :
    IsTrichotomous (WithBot α) (· > ·) where
  trichotomous x y := by cases x <;> cases y <;> simp; simpa using trichotomous_of (· > ·) ..

Trichotomy of Strict Greater-Than Relation on $\alpha$ with Bottom Element

Informal description

For any preorder $\alpha$ with a trichotomous strict greater-than relation $>$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) also has a trichotomous strict greater-than relation $>$.

WithBot.isWellOrder.gt instance

[Preorder α] [h : IsWellOrder α (· > ·)] : IsWellOrder (WithBot α) (· > ·)

Full source

instance _root_.WithBot.isWellOrder.gt [Preorder α] [h : IsWellOrder α (· > ·)] :
    IsWellOrder (WithBot α) (· > ·) where
  trichotomous x y := by cases x <;> cases y <;> simp; simpa using trichotomous_of (· > ·) ..

Well-Founded Strict Greater-Than Relation on $\alpha$ with Bottom Element

Informal description

For any preorder $\alpha$ with a well-founded strict greater-than relation $>$, the type $\text{WithBot }\alpha$ (which is $\alpha$ with an added bottom element $\bot$) also has a well-founded strict greater-than relation $>$.

WithTop.instDenselyOrderedOfNoMaxOrder instance

[LT α] [DenselyOrdered α] [NoMaxOrder α] : DenselyOrdered (WithTop α)

Full source

instance [LT α] [DenselyOrdered α] [NoMaxOrder α] : DenselyOrdered (WithTop α) :=
  OrderDual.denselyOrdered (WithBot αᵒᵈ)

Densely Ordered Structure on $\alpha$ Extended with a Top Element

Informal description

For any densely ordered type $\alpha$ with no maximal elements, the type $\text{WithTop}\ \alpha$ (which is $\alpha$ with an added top element $\top$) is also densely ordered. This means that for any two elements $a < b$ in $\text{WithTop}\ \alpha$, there exists an element $x$ such that $a < x < b$.

WithTop.lt_iff_exists_coe_btwn theorem

[Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α} : a < b ↔ ∃ x : α, a < ↑x ∧ ↑x < b

Full source

theorem lt_iff_exists_coe_btwn [Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α} :
    a < b ↔ ∃ x : α, a < ↑x ∧ ↑x < b :=
  ⟨fun h =>
    let ⟨_, hy⟩ := exists_between h
    let ⟨x, hx⟩ := lt_iff_exists_coe.1 hy.2
    ⟨x, hx.1 ▸ hy⟩,
    fun ⟨_, hx⟩ => lt_trans hx.1 hx.2⟩

Characterization of Inequality in $\text{WithTop}\ \alpha$ via Intermediate Element from $\alpha$

Informal description

Let $\alpha$ be a preorder that is densely ordered and has no maximal elements. For any two elements $a, b$ in $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$), the inequality $a < b$ holds if and only if there exists an element $x \in \alpha$ such that $a < x$ and $x < b$ in $\text{WithTop}\ \alpha$.

WithTop.noBotOrder instance

[LE α] [NoBotOrder α] [Nonempty α] : NoBotOrder (WithTop α)

Full source

instance noBotOrder [LE α] [NoBotOrder α] [Nonempty α] : NoBotOrder (WithTop α) where
  exists_not_ge := fun
    | ⊤ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) => let ⟨b, hba⟩ := exists_not_ge a; ⟨b, mod_cast hba⟩

No Bottom Elements in $\alpha$ Extended with Top

Informal description

For any type $\alpha$ with a preorder and no bottom elements, the type $\alpha$ extended with a top element $\top$ also has no bottom elements.

WithTop.noMinOrder instance

[LT α] [NoMinOrder α] [Nonempty α] : NoMinOrder (WithTop α)

Full source

instance noMinOrder [LT α] [NoMinOrder α] [Nonempty α] : NoMinOrder (WithTop α) where
  exists_lt := fun
    | ⊤ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) => let ⟨b, hab⟩ := exists_lt a; ⟨b, mod_cast hab⟩

No Minimal Elements in $\alpha$ Extended with Top

Informal description

For any type $\alpha$ with a strict order relation $<$ and no minimal elements, the type $\alpha$ extended with a top element $\top$ also has no minimal elements.

WithBot.toDual_symm_apply theorem

(a : WithTop αᵒᵈ) : WithBot.toDual.symm a = WithTop.ofDual a

Full source

@[simp]
lemma toDual_symm_apply (a : WithTop αᵒᵈ) : WithBot.toDual.symm a = WithTop.ofDual a :=
  rfl

Inverse of `WithBot.toDual` Equals `WithTop.ofDual`

Informal description

For any element $a$ in the type `WithTop αᵒᵈ`, the inverse of the equivalence `WithBot.toDual` applied to $a$ is equal to the equivalence `WithTop.ofDual` applied to $a$. In other words, the inverse of the bijection between `WithBot α` and `WithTop αᵒᵈ` coincides with the bijection from `WithTop αᵒᵈ` to `WithBot α`.

WithBot.ofDual_symm_apply theorem

(a : WithTop α) : WithBot.ofDual.symm a = WithTop.toDual a

Full source

@[simp]
lemma ofDual_symm_apply (a : WithTop α) : WithBot.ofDual.symm a = WithTop.toDual a :=
  rfl

Inverse of `WithBot.ofDual` Equals `WithTop.toDual`

Informal description

For any element $a$ in the type `WithTop α`, the inverse of the equivalence `WithBot.ofDual` applied to $a$ is equal to the equivalence `WithTop.toDual` applied to $a$. In other words, the inverse of the map that converts `WithBot αᵒᵈ` to `WithTop α` is the same as the map that converts `WithTop α` to `WithBot αᵒᵈ`.

WithBot.toDual_apply_bot theorem

: WithBot.toDual (⊥ : WithBot α) = ⊤

Full source

@[simp] lemma toDual_apply_bot : WithBot.toDual (⊥ : WithBot α) = ⊤ := rfl

Bottom-to-Top Mapping in Dual Equivalence: $\text{WithBot.toDual}(\bot) = \top$

Informal description

The equivalence `WithBot.toDual` maps the bottom element $\bot$ of `WithBot α` to the top element $\top$ of `WithTop αᵒᵈ$, i.e., $\text{WithBot.toDual}(\bot) = \top$.

WithBot.ofDual_apply_bot theorem

: WithBot.ofDual (⊥ : WithBot α) = ⊤

Full source

@[simp] lemma ofDual_apply_bot : WithBot.ofDual (⊥ : WithBot α) = ⊤ := rfl

Bottom-to-Top Mapping in Order Dual with `WithBot` and `WithTop`

Informal description

The equivalence `WithBot.ofDual` maps the bottom element $\bot$ of `WithBot α` to the top element $\top$ of `WithTop αᵒᵈ$, i.e., $\text{WithBot.ofDual}(\bot) = \top$.

WithBot.toDual_apply_coe theorem

(a : α) : WithBot.toDual (a : WithBot α) = toDual a

Full source

@[simp] lemma toDual_apply_coe (a : α) : WithBot.toDual (a : WithBot α) = toDual a := rfl

Equivalence of `WithBot.toDual` on elements of $\alpha$

Informal description

For any element $a$ of type $\alpha$, the equivalence `WithBot.toDual` maps the element $a$ in `WithBot α` to its dual element in `WithTop αᵒᵈ`, i.e., $\text{WithBot.toDual}(a) = \text{toDual}(a)$.

WithBot.ofDual_apply_coe theorem

(a : αᵒᵈ) : WithBot.ofDual (a : WithBot αᵒᵈ) = ofDual a

Full source

@[simp] lemma ofDual_apply_coe (a : αᵒᵈ) : WithBot.ofDual (a : WithBot αᵒᵈ) = ofDual a := rfl

Equivalence between `WithBot αᵒᵈ` and `WithTop α` on elements

Informal description

For any element $a$ in the order-dual type $\alpha^\mathrm{op}$, the equivalence `WithBot.ofDual` maps the element `a` (viewed as an element of `WithBot αᵒᵈ`) to its corresponding element `ofDual a` in `WithTop α$.

WithBot.map_toDual theorem

(f : αᵒᵈ → βᵒᵈ) (a : WithTop α) : WithBot.map f (WithTop.toDual a) = a.map (toDual ∘ f)

Full source

lemma map_toDual (f : αᵒᵈ → βᵒᵈ) (a : WithTop α) :
    WithBot.map f (WithTop.toDual a) = a.map (toDualtoDual ∘ f) := rfl

Compatibility of $\text{WithBot.map}$ with duality and $\text{WithTop}$ mapping

Informal description

For any function $f : \alpha^\text{op} \to \beta^\text{op}$ and any element $a$ in $\text{WithTop}\ \alpha$, the map $\text{WithBot.map}\ f$ applied to the dual of $a$ (via $\text{WithTop.toDual}$) is equal to the $\text{WithTop}$ map of $a$ under the composition $\text{toDual} \circ f$. In symbols: $$\text{WithBot.map}\ f\ (\text{WithTop.toDual}\ a) = a.\text{map}\ (\text{toDual} \circ f)$$

WithBot.map_ofDual theorem

(f : α → β) (a : WithTop αᵒᵈ) : WithBot.map f (WithTop.ofDual a) = a.map (ofDual ∘ f)

Full source

lemma map_ofDual (f : α → β) (a : WithTop αᵒᵈ) :
    WithBot.map f (WithTop.ofDual a) = a.map (ofDualofDual ∘ f) := rfl

Compatibility of `WithBot.map` with Dualization: $\text{WithBot.map} f \circ \text{WithTop.ofDual} = \text{map} (\text{ofDual} \circ f)$

Informal description

Let $f : \alpha \to \beta$ be a function and let $a$ be an element of $\text{WithTop} \alpha^\text{op}$. Then the map $\text{WithBot.map} f$ applied to the dual of $a$ (via $\text{WithTop.ofDual}$) is equal to mapping the composition $\text{ofDual} \circ f$ over $a$.

WithBot.toDual_map theorem

(f : α → β) (a : WithBot α) : WithBot.toDual (WithBot.map f a) = map (toDual ∘ f ∘ ofDual) (WithBot.toDual a)

Full source

lemma toDual_map (f : α → β) (a : WithBot α) :
    WithBot.toDual (WithBot.map f a) = map (toDualtoDual ∘ f ∘ ofDual) (WithBot.toDual a) := rfl

Dual Image of Lifted Function in WithBot and WithTop

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \text{WithBot} \alpha$, the dual of the image of $a$ under the lifted map $\text{WithBot.map} f$ is equal to the image of the dual of $a$ under the composition $\text{toDual} \circ f \circ \text{ofDual}$ in $\text{WithTop} \alpha^\text{op}$. In symbols: $$(\text{WithBot.map} f(a))^\text{op} = \text{map} (f^\text{op}) (a^\text{op})$$ where $f^\text{op} = \text{toDual} \circ f \circ \text{ofDual}$ is the dualized function and $a^\text{op}$ is the dual of $a$.

WithBot.ofDual_map theorem

 (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ) : WithBot.ofDual (WithBot.map f a) = map (ofDual ∘ f ∘ toDual) (WithBot.ofDual a)

Full source

lemma ofDual_map (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ) :
    WithBot.ofDual (WithBot.map f a) = map (ofDualofDual ∘ f ∘ toDual) (WithBot.ofDual a) := rfl

Commutativity of `WithBot.ofDual` with `map` for Order Duals

Informal description

For any function $f : \alpha^\text{op} \to \beta^\text{op}$ and any element $a \in \text{WithBot}(\alpha^\text{op})$, the following equality holds: \[ \text{WithBot.ofDual}(\text{WithBot.map}(f)(a)) = \text{map}(\text{ofDual} \circ f \circ \text{toDual})(\text{WithBot.ofDual}(a)) \] Here, $\text{WithBot.ofDual}$ is the equivalence between $\text{WithBot}(\alpha^\text{op})$ and $\text{WithTop}(\alpha)$, and $\text{ofDual}$ and $\text{toDual}$ are the canonical maps between $\alpha$ and its order dual $\alpha^\text{op}$.

WithBot.toDual_le_iff theorem

{x : WithBot α} {y : WithTop αᵒᵈ} : x.toDual ≤ y ↔ WithTop.ofDual y ≤ x

Full source

lemma WithBot.toDual_le_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x.toDual ≤ y ↔ WithTop.ofDual y ≤ x := by
  cases x <;> cases y <;> simp [toDual_le]

Dual Order Comparison in $\text{WithBot}\ \alpha$ and $\text{WithTop}\ \alpha^\text{op}$

Informal description

For any element $x$ in $\text{WithBot}\ \alpha$ and any element $y$ in $\text{WithTop}\ \alpha^\text{op}$, the dual of $x$ is less than or equal to $y$ if and only if the undual of $y$ is less than or equal to $x$. In other words: \[ \text{toDual}(x) \leq y \leftrightarrow \text{ofDual}(y) \leq x \]

WithBot.le_toDual_iff theorem

{x : WithTop αᵒᵈ} {y : WithBot α} : x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Full source

lemma WithBot.le_toDual_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x := by cases x <;> cases y <;> simp [le_toDual]

Inequality Equivalence between $\text{WithTop}\ \alpha^\text{op}$ and $\text{WithBot}\ \alpha$ via Duality

Informal description

For any element $x$ in $\text{WithTop}\ \alpha^\text{op}$ and any element $y$ in $\text{WithBot}\ \alpha$, the inequality $x \leq \text{toDual}\ y$ holds if and only if $y \leq \text{ofDual}\ x$.

WithBot.toDual_le_toDual_iff theorem

{x y : WithBot α} : x.toDual ≤ y.toDual ↔ y ≤ x

Full source

@[simp]
lemma WithBot.toDual_le_toDual_iff {x y : WithBot α} : x.toDual ≤ y.toDual ↔ y ≤ x := by
  cases x <;> cases y <;> simp

Dual Order Reversal in WithBot and WithTop

Informal description

For any elements $x, y$ in $\text{WithBot}\ \alpha$, the inequality $x^\ast \leq y^\ast$ holds in $\text{WithTop}\ \alpha^\ast$ if and only if $y \leq x$ holds in $\text{WithBot}\ \alpha$, where $x^\ast$ denotes the dual element of $x$ in the order dual.

WithBot.ofDual_le_iff theorem

{x : WithBot αᵒᵈ} {y : WithTop α} : WithBot.ofDual x ≤ y ↔ y.toDual ≤ x

Full source

lemma WithBot.ofDual_le_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    WithBot.ofDualWithBot.ofDual x ≤ y ↔ y.toDual ≤ x := by cases x <;> cases y <;> simp [toDual_le]

Inequality between Dual Elements in $\text{WithBot}\ \alpha^\text{op}$ and $\text{WithTop}\ \alpha$

Informal description

For any element $x$ in $\text{WithBot}\ \alpha^\text{op}$ and any element $y$ in $\text{WithTop}\ \alpha$, the inequality $\text{WithBot.ofDual}\ x \leq y$ holds if and only if the dual of $y$ is less than or equal to $x$ in $\text{WithBot}\ \alpha^\text{op}$.

WithBot.le_ofDual_iff theorem

{x : WithTop α} {y : WithBot αᵒᵈ} : x ≤ WithBot.ofDual y ↔ y ≤ x.toDual

Full source

lemma WithBot.le_ofDual_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    x ≤ WithBot.ofDual y ↔ y ≤ x.toDual := by cases x <;> cases y <;> simp [le_toDual]

Inequality between $\text{WithTop}\ \alpha$ and $\text{WithBot}\ \alpha^\text{op}$ via duality

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ and any element $y$ in $\text{WithBot}\ \alpha^\text{op}$, the inequality $x \leq \text{WithBot.ofDual}\ y$ holds if and only if $y \leq x^\text{op}$.

WithBot.ofDual_le_ofDual_iff theorem

{x y : WithBot αᵒᵈ} : WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

Full source

@[simp]
lemma WithBot.ofDual_le_ofDual_iff {x y : WithBot αᵒᵈ} :
    WithBot.ofDualWithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x := by cases x <;> cases y <;> simp

Order Reversal in Dualization of `WithBot` and `WithTop`

Informal description

For any elements $x, y$ in the type `WithBot αᵒᵈ` (where `αᵒᵈ` is the order dual of `α`), the inequality $\text{ofDual}(x) \leq \text{ofDual}(y)$ holds in `WithTop α` if and only if $y \leq x$ holds in `WithBot αᵒᵈ$.

WithTop.toDual_le_iff theorem

{x : WithTop α} {y : WithBot αᵒᵈ} : x.toDual ≤ y ↔ WithBot.ofDual y ≤ x

Full source

lemma WithTop.toDual_le_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    x.toDual ≤ y ↔ WithBot.ofDual y ≤ x := by cases x <;> cases y <;> simp [toDual_le]

Inequality Equivalence between Dual Elements in $\text{WithTop}\ \alpha$ and $\text{WithBot}\ \alpha^\text{op}$

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ and any element $y$ in $\text{WithBot}\ \alpha^\text{op}$, the inequality $x^\text{op} \leq y$ holds if and only if the corresponding element $\text{ofDual}\ y$ in $\text{WithTop}\ \alpha$ satisfies $\text{ofDual}\ y \leq x$.

WithTop.le_toDual_iff theorem

{x : WithBot αᵒᵈ} {y : WithTop α} : x ≤ WithTop.toDual y ↔ y ≤ WithBot.ofDual x

Full source

lemma WithTop.le_toDual_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    x ≤ WithTop.toDual y ↔ y ≤ WithBot.ofDual x := by cases x <;> cases y <;> simp [le_toDual]

Order Reversal in Dualized WithBot and WithTop

Informal description

For any element $x$ in $\text{WithBot}\ \alpha^\text{op}$ and any element $y$ in $\text{WithTop}\ \alpha$, the inequality $x \leq \text{WithTop.toDual}\ y$ holds if and only if $y \leq \text{WithBot.ofDual}\ x$.

WithTop.toDual_le_toDual_iff theorem

{x y : WithTop α} : x.toDual ≤ y.toDual ↔ y ≤ x

Full source

@[simp]
lemma WithTop.toDual_le_toDual_iff {x y : WithTop α} : x.toDual ≤ y.toDual ↔ y ≤ x := by
  cases x <;> cases y <;> simp [le_toDual]

Inequality Reversal under Dualization: $x^\text{dual} \leq y^\text{dual} \leftrightarrow y \leq x$ in `WithTop` and `WithBot`

Informal description

For any elements $x, y$ in the type `WithTop α` (which is $\alpha$ extended with a top element $\top$), the inequality $x^\text{dual} \leq y^\text{dual}$ holds in `WithBot αᵒᵈ` (the dual order of $\alpha$ extended with a bottom element $\bot$) if and only if $y \leq x$ holds in `WithTop α$.

WithTop.ofDual_le_iff theorem

{x : WithTop αᵒᵈ} {y : WithBot α} : WithTop.ofDual x ≤ y ↔ y.toDual ≤ x

Full source

lemma WithTop.ofDual_le_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    WithTop.ofDualWithTop.ofDual x ≤ y ↔ y.toDual ≤ x := by cases x <;> cases y <;> simp [toDual_le]

Inequality Characterization via Dual Order in $\text{WithTop}$ and $\text{WithBot}$

Informal description

For any element $x$ in $\text{WithTop}\ \alpha^\text{op}$ and any element $y$ in $\text{WithBot}\ \alpha$, the inequality $\text{WithTop.ofDual}\ x \leq y$ holds if and only if $y^\text{op} \leq x$ in $\text{WithTop}\ \alpha^\text{op}$.

WithTop.le_ofDual_iff theorem

{x : WithBot α} {y : WithTop αᵒᵈ} : x ≤ WithTop.ofDual y ↔ y ≤ x.toDual

Full source

lemma WithTop.le_ofDual_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x ≤ WithTop.ofDual y ↔ y ≤ x.toDual := by cases x <;> cases y <;> simp [le_toDual]

Order Reversal via Dualization: $x \leq \text{ofDual}\ y \leftrightarrow y \leq x^\text{op}$

Informal description

For any element $x$ in $\text{WithBot}\ \alpha$ and any element $y$ in $\text{WithTop}\ \alpha^\text{op}$, the inequality $x \leq \text{WithTop.ofDual}\ y$ holds if and only if $y \leq x^\text{op}$ in $\text{WithTop}\ \alpha^\text{op}$.

WithTop.ofDual_le_ofDual_iff theorem

{x y : WithTop αᵒᵈ} : WithTop.ofDual x ≤ WithTop.ofDual y ↔ y ≤ x

Full source

@[simp]
lemma WithTop.ofDual_le_ofDual_iff {x y : WithTop αᵒᵈ} :
    WithTop.ofDualWithTop.ofDual x ≤ WithTop.ofDual y ↔ y ≤ x :=  by cases x <;> cases y <;> simp

Order Reversal in Dual Extended Types: $\text{ofDual}(x) \leq \text{ofDual}(y) \leftrightarrow y \leq x$

Informal description

For any elements $x, y$ in the order dual of $\alpha$ extended with a top element, the inequality $\text{ofDual}(x) \leq \text{ofDual}(y)$ holds in $\text{WithBot}(\alpha)$ if and only if $y \leq x$ holds in $\text{WithTop}(\alpha^\text{op})$.

WithBot.toDual_lt_iff theorem

{x : WithBot α} {y : WithTop αᵒᵈ} : x.toDual < y ↔ WithTop.ofDual y < x

Full source

lemma WithBot.toDual_lt_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x.toDual < y ↔ WithTop.ofDual y < x := by cases x <;> cases y <;> simp [toDual_lt]

Order Reversal via Dualization: $x^\text{op} < y \leftrightarrow \text{ofDual}(y) < x$

Informal description

For any element $x$ in $\text{WithBot}(\alpha)$ and any element $y$ in $\text{WithTop}(\alpha^\text{op})$, the inequality $x^\text{op} < y$ holds if and only if $\text{ofDual}(y) < x$ holds in $\text{WithBot}(\alpha)$.

WithBot.lt_toDual_iff theorem

{x : WithTop αᵒᵈ} {y : WithBot α} : x < y.toDual ↔ y < WithTop.ofDual x

Full source

lemma WithBot.lt_toDual_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    x < y.toDual ↔ y < WithTop.ofDual x := by cases x <;> cases y <;> simp [lt_toDual]

Order Reversal in Dual Extended Types: $x < \text{toDual}(y) \leftrightarrow y < \text{ofDual}(x)$

Informal description

For any element $x$ in the order dual of $\alpha$ extended with a top element and any element $y$ in $\alpha$ extended with a bottom element, the inequality $x < \text{toDual}(y)$ holds in $\text{WithTop}(\alpha^\text{op})$ if and only if $y < \text{ofDual}(x)$ holds in $\text{WithBot}(\alpha)$.

WithBot.toDual_lt_toDual_iff theorem

{x y : WithBot α} : x.toDual < y.toDual ↔ y < x

Full source

@[simp]
lemma WithBot.toDual_lt_toDual_iff {x y : WithBot α} : x.toDual < y.toDual ↔ y < x := by
  cases x <;> cases y <;> simp

Dual Order Reversal in `WithBot` and `WithTop`

Informal description

For any elements $x, y$ in `WithBot α`, the dual of $x$ is less than the dual of $y$ in `WithTop αᵒᵈ` if and only if $y$ is less than $x$ in `WithBot α`. That is, $x^\ast < y^\ast \leftrightarrow y < x$, where $x^\ast$ denotes the dual of $x$ in the order-dual type.

WithBot.ofDual_lt_iff theorem

{x : WithBot αᵒᵈ} {y : WithTop α} : WithBot.ofDual x < y ↔ y.toDual < x

Full source

lemma WithBot.ofDual_lt_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    WithBot.ofDualWithBot.ofDual x < y ↔ y.toDual < x := by cases x <;> cases y <;> simp [toDual_lt]

Inequality between Dual Elements in $\text{WithBot}$ and $\text{WithTop}$

Informal description

For any element $x$ in $\text{WithBot}(\alpha^\text{op})$ and $y$ in $\text{WithTop}(\alpha)$, the inequality $\text{WithBot.ofDual}(x) < y$ holds if and only if $\text{WithTop.toDual}(y) < x$.

WithBot.lt_ofDual_iff theorem

{x : WithTop α} {y : WithBot αᵒᵈ} : x < WithBot.ofDual y ↔ y < x.toDual

Full source

lemma WithBot.lt_ofDual_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    x < WithBot.ofDual y ↔ y < x.toDual := by cases x <;> cases y <;> simp [lt_toDual]

Order Reversal in Extended Types via Dual Equivalence

Informal description

Let $\alpha$ be a type with an order. For any element $x$ in $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$) and any element $y$ in $\text{WithBot}\ \alpha^\text{op}$ (the order dual of $\alpha$ extended with a bottom element $\bot$), we have that $x$ is less than the image of $y$ under the equivalence $\text{WithBot.ofDual}$ if and only if $y$ is less than the dual image of $x$ under $\text{WithTop.toDual}$. In symbols: $$x < \text{WithBot.ofDual}(y) \leftrightarrow y < \text{WithTop.toDual}(x)$$

WithBot.ofDual_lt_ofDual_iff theorem

{x y : WithBot αᵒᵈ} : WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Full source

@[simp]
lemma WithBot.ofDual_lt_ofDual_iff {x y : WithBot αᵒᵈ} :
    WithBot.ofDualWithBot.ofDual x < WithBot.ofDual y ↔ y < x := by cases x <;> cases y <;> simp

Inequality Reversal under Dualization in `WithBot αᵒᵈ`

Informal description

For any elements $x, y$ in the type `WithBot αᵒᵈ` (the type $\alpha$ with a bottom element and the order reversed), the inequality $\text{ofDual}\ x < \text{ofDual}\ y$ holds if and only if $y < x$ in the original order.

WithTop.toDual_lt_iff theorem

{x : WithTop α} {y : WithBot αᵒᵈ} : WithTop.toDual x < y ↔ WithBot.ofDual y < x

Full source

lemma WithTop.toDual_lt_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    WithTop.toDualWithTop.toDual x < y ↔ WithBot.ofDual y < x := by cases x <;> cases y <;> simp [toDual_lt]

Dual Order Inequality in $\text{WithTop}\ \alpha$ and $\text{WithBot}\ \alpha^\text{op}$

Informal description

For any element $x$ in $\text{WithTop}\ \alpha$ and any element $y$ in $\text{WithBot}\ \alpha^\text{op}$, the dual of $x$ is less than $y$ if and only if the dual of $y$ is less than $x$ in the original order. In other words, the following equivalence holds: \[ \text{toDual}(x) < y \leftrightarrow \text{ofDual}(y) < x. \]

WithTop.lt_toDual_iff theorem

{x : WithBot αᵒᵈ} {y : WithTop α} : x < WithTop.toDual y ↔ y < WithBot.ofDual x

Full source

lemma WithTop.lt_toDual_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    x < WithTop.toDual y ↔ y < WithBot.ofDual x := by cases x <;> cases y <;> simp [lt_toDual]

Inequality Equivalence between $\text{WithBot}\ \alpha^\text{op}$ and $\text{WithTop}\ \alpha$ via Dualization

Informal description

For any element $x$ in $\text{WithBot}\ \alpha^\text{op}$ and any element $y$ in $\text{WithTop}\ \alpha$, the inequality $x < \text{WithTop.toDual}\ y$ holds if and only if $y < \text{WithBot.ofDual}\ x$.

WithTop.toDual_lt_toDual_iff theorem

{x y : WithTop α} : WithTop.toDual x < WithTop.toDual y ↔ y < x

Full source

@[simp]
lemma WithTop.toDual_lt_toDual_iff {x y : WithTop α} :
    WithTop.toDualWithTop.toDual x < WithTop.toDual y ↔ y < x := by cases x <;> cases y <;> simp

Order Reversal under Duality for `WithTop` Elements

Informal description

For any elements $x$ and $y$ in the type `WithTop α`, the dual of $x$ is less than the dual of $y$ in `WithBot αᵒᵈ` if and only if $y$ is less than $x$ in `WithTop α$. In other words, the equivalence `WithTop.toDual` reverses the order relation between elements when mapping from `WithTop α` to `WithBot αᵒᵈ`.

WithTop.ofDual_lt_iff theorem

{x : WithTop αᵒᵈ} {y : WithBot α} : WithTop.ofDual x < y ↔ WithBot.toDual y < x

Full source

lemma WithTop.ofDual_lt_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    WithTop.ofDualWithTop.ofDual x < y ↔ WithBot.toDual y < x := by cases x <;> cases y <;> simp [toDual_lt]

Inequality Preservation under Dualization in Extended Types

Informal description

For any element $x$ in $\text{WithTop}\ \alpha^\text{op}$ and any element $y$ in $\text{WithBot}\ \alpha$, the inequality $\text{ofDual}\ x < y$ holds if and only if $\text{toDual}\ y < x$, where $\text{ofDual}$ and $\text{toDual}$ are the canonical equivalences between $\text{WithTop}\ \alpha^\text{op}$ and $\text{WithBot}\ \alpha$.

WithTop.lt_ofDual_iff theorem

{x : WithBot α} {y : WithTop αᵒᵈ} : x < WithTop.ofDual y ↔ y < WithBot.toDual x

Full source

lemma WithTop.lt_ofDual_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x < WithTop.ofDual y ↔ y < WithBot.toDual x := by cases x <;> cases y <;> simp [lt_toDual]

Inequality between `WithBot` and dual `WithTop` elements

Informal description

For any element $x$ in `WithBot α` and any element $y$ in the order dual of `WithTop α`, the inequality $x < \text{ofDual}(y)$ holds if and only if $y < \text{toDual}(x)$.

WithTop.ofDual_lt_ofDual_iff theorem

{x y : WithTop αᵒᵈ} : WithTop.ofDual x < WithTop.ofDual y ↔ y < x

Full source

@[simp]
lemma WithTop.ofDual_lt_ofDual_iff {x y : WithTop αᵒᵈ} :
    WithTop.ofDualWithTop.ofDual x < WithTop.ofDual y ↔ y < x := by cases x <;> cases y <;> simp

Order Reversal under Dualization in $\text{WithTop}\ \alpha^\text{op}$

Informal description

For any elements $x$ and $y$ in $\text{WithTop}\ \alpha^\text{op}$, the inequality $\text{WithTop.ofDual}\ x < \text{WithTop.ofDual}\ y$ holds if and only if $y < x$ in $\text{WithTop}\ \alpha^\text{op}$.

Main declarations