Mathlib.Order.SuccPred.WithBot

WithBot.succ definition

(a : WithBot α) : α

Full source

/-- The successor of `a : WithBot α` as an element of `α`. -/
def succ (a : WithBot α) : α := a.recBotCoe ⊥ Order.succ

Successor function on `WithBot α`

Informal description

The successor function on `WithBot α` maps an element `a : WithBot α` to its successor in `α`. Specifically: - If `a` is `⊥` (the bottom element), its successor is `⊥`. - If `a` is of the form `(b : α)`, its successor is the successor of `b` in the order on `α`.

WithBot.succ_bot theorem

: succ (⊥ : WithBot α) = ⊥

Full source

/-- Not to be confused with `WithBot.orderSucc_bot`, which is about `Order.succ`. -/
@[simp] lemma succ_bot : succ (⊥ : WithBot α) = ⊥ := rfl

Successor of Bottom in $\text{WithBot} \, \alpha$ is Bottom

Informal description

The successor of the bottom element $\bot$ in $\text{WithBot} \, \alpha$ is $\bot$ itself, i.e., $\text{succ}(\bot) = \bot$.

WithBot.succ_coe theorem

(a : α) : succ (a : WithBot α) = Order.succ a

Full source

/-- Not to be confused with `WithBot.orderSucc_coe`, which is about `Order.succ`. -/
@[simp] lemma succ_coe (a : α) : succ (a : WithBot α) = Order.succ a := rfl

Equality of Successor Functions on $\text{WithBot} \, \alpha$ and $\alpha$

Informal description

For any element $a$ of type $\alpha$, the successor of $a$ in $\text{WithBot} \, \alpha$ (denoted as $\text{succ}(a)$) is equal to the successor of $a$ in the order on $\alpha$ (denoted as $\text{Order.succ}(a)$), i.e., $\text{succ}(a) = \text{Order.succ}(a)$.

WithBot.succ_eq_succ theorem

: ∀ a : WithBot α, succ a = Order.succ a

Full source

lemma succ_eq_succ : ∀ a : WithBot α, succ a = Order.succ a
  | ⊥ => rfl
  | (a : α) => rfl

Equality of Successor Functions on $\text{WithBot} \, \alpha$ and $\alpha$

Informal description

For any element $a$ in $\text{WithBot} \, \alpha$, the successor of $a$ in $\text{WithBot} \, \alpha$ is equal to the successor of $a$ in the order on $\alpha$, i.e., $\text{succ}(a) = \text{Order.succ}(a)$.

WithBot.succ_mono theorem

: Monotone (succ : WithBot α → α)

Full source

lemma succ_mono : Monotone (succ : WithBot α → α)
  | ⊥, _, _ => by simp
  | (a : α), ⊥, hab => by simp at hab
  | (a : α), (b : α), hab => Order.succ_le_succ (by simpa using hab)

Monotonicity of the Successor Function on `WithBot α`

Informal description

The successor function on `WithBot α` is monotone, i.e., for any elements `x, y : WithBot α`, if `x ≤ y`, then `succ x ≤ succ y`.

WithBot.succ_strictMono theorem

[NoMaxOrder α] : StrictMono (succ : WithBot α → α)

Full source

lemma succ_strictMono [NoMaxOrder α] : StrictMono (succ : WithBot α → α)
  | ⊥, (b : α), hab => by simp
  | (a : α), (b : α), hab => Order.succ_lt_succ (by simpa using hab)

Strict Monotonicity of Successor Function on $\text{WithBot} \, \alpha$ under NoMaxOrder Condition

Informal description

For any type $\alpha$ with no maximal element (i.e., a `NoMaxOrder`), the successor function on $\text{WithBot} \, \alpha$ is strictly monotone. That is, for any $x, y \in \text{WithBot} \, \alpha$, if $x < y$, then $\text{succ}(x) < \text{succ}(y)$.

WithBot.succ_le_succ theorem

(hxy : x ≤ y) : x.succ ≤ y.succ

Full source

@[gcongr] lemma succ_le_succ (hxy : x ≤ y) : x.succ ≤ y.succ := succ_mono hxy

Successor Preserves Order in $\text{WithBot} \, \alpha$

Informal description

For any elements $x, y$ in $\text{WithBot} \, \alpha$, if $x \leq y$, then the successor of $x$ is less than or equal to the successor of $y$, i.e., $\text{succ}(x) \leq \text{succ}(y)$.

WithBot.succ_lt_succ theorem

[NoMaxOrder α] (hxy : x < y) : x.succ < y.succ

Full source

@[gcongr] lemma succ_lt_succ [NoMaxOrder α] (hxy : x < y) : x.succ < y.succ := succ_strictMono hxy

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

Informal description

For any type $\alpha$ with no maximal element (i.e., a `NoMaxOrder`), and for any elements $x, y$ in $\text{WithBot} \, \alpha$, if $x < y$, then the successor of $x$ is strictly less than the successor of $y$, i.e., $\text{succ}(x) < \text{succ}(y)$.

WithBot.succ_eq_bot theorem

(a : WithBot α) : WithBot.succ a = ⊥ ↔ a = ⊥

Full source

@[simp]
theorem succ_eq_bot (a : WithBot α) : WithBot.succWithBot.succ a = ⊥ ↔ a = ⊥ := by
  cases a
  · simp
  · simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false]
    apply ne_of_gt
    by_contra! h
    have h₂ : _ = ⊥ := le_bot_iff.mp ((Order.le_succ _).trans h)
    exact not_isMax_bot (h₂ ▸ Order.max_of_succ_le (h.trans bot_le))

Characterization of Bottom Element via Successor: $\text{succ}(a) = \bot \leftrightarrow a = \bot$

Informal description

For any element $a$ in $\text{WithBot} \, \alpha$, the successor of $a$ is equal to the bottom element $\bot$ if and only if $a$ itself is $\bot$.

WithTop.pred definition

(a : WithTop α) : α

Full source

/-- The predecessor of `a : WithTop α` as an element of `α`. -/
def pred (a : WithTop α) : α := a.recTopCoe ⊤ Order.pred

Predecessor function on `WithTop α`

Informal description

The function maps an element `a` of the type `WithTop α` (which is `α` extended with a top element `⊤`) to its predecessor in `α`. If `a` is the top element `⊤`, the function returns `⊤`. Otherwise, it returns the predecessor of `a` in `α` using the `Order.pred` function.

WithTop.pred_top theorem

: pred (⊤ : WithTop α) = ⊤

Full source

/-- Not to be confused with `WithTop.orderPred_top`, which is about `Order.pred`. -/
@[simp] lemma pred_top : pred (⊤ : WithTop α) = ⊤ := rfl

Predecessor of Top Element in $\text{WithTop}\ \alpha$ is Top

Informal description

The predecessor function applied to the top element $\top$ in $\text{WithTop}\ \alpha$ returns $\top$, i.e., $\operatorname{pred}(\top) = \top$.

WithTop.pred_coe theorem

(a : α) : pred (a : WithTop α) = Order.pred a

Full source

/-- Not to be confused with `WithTop.orderPred_coe`, which is about `Order.pred`. -/
@[simp] lemma pred_coe (a : α) : pred (a : WithTop α) = Order.pred a := rfl

Predecessor Function Commutes with Embedding in $\text{WithTop}\ \alpha$

Informal description

For any element $a$ of type $\alpha$, the predecessor function applied to the embedding of $a$ in $\text{WithTop}\ \alpha$ equals the predecessor of $a$ in $\alpha$, i.e., $\operatorname{pred}(a) = \operatorname{Order.pred}(a)$.

WithTop.pred_eq_pred theorem

: ∀ a : WithTop α, pred a = Order.pred a

Full source

lemma pred_eq_pred : ∀ a : WithTop α, pred a = Order.pred a
  | ⊤ => rfl
  | (a : α) => rfl

Predecessor Function Equality on $\text{WithTop}\ \alpha$

Informal description

For any element $a$ in $\text{WithTop}\ \alpha$, the predecessor function $\operatorname{pred}$ on $\text{WithTop}\ \alpha$ coincides with the predecessor function $\operatorname{Order.pred}$ on $\alpha$, i.e., $\operatorname{pred}(a) = \operatorname{Order.pred}(a)$.

WithTop.pred_mono theorem

: Monotone (pred : WithTop α → α)

Full source

lemma pred_mono : Monotone (pred : WithTop α → α)
  | _, ⊤, _ => by simp
  | ⊤, (a : α), hab => by simp at hab
  | (a : α), (b : α), hab => Order.pred_le_pred (by simpa using hab)

Monotonicity of Predecessor Function on Extended Type with Top

Informal description

The predecessor function $\operatorname{pred} : \text{WithTop}\ \alpha \to \alpha$ is monotone, meaning that for any $x, y \in \text{WithTop}\ \alpha$, if $x \leq y$ then $\operatorname{pred}(x) \leq \operatorname{pred}(y)$.

WithTop.pred_strictMono theorem

[NoMinOrder α] : StrictMono (pred : WithTop α → α)

Full source

lemma pred_strictMono [NoMinOrder α] : StrictMono (pred : WithTop α → α)
  | (b : α), ⊤, hab => by simp
  | (a : α), (b : α), hab => Order.pred_lt_pred (by simpa using hab)

Strict Monotonicity of Predecessor Function on Extended Type with Top

Informal description

Let $\alpha$ be a type with a strict order and no minimal element. Then the predecessor function $\operatorname{pred} : \text{WithTop}\ \alpha \to \alpha$ is strictly monotone, meaning that for any $x, y \in \text{WithTop}\ \alpha$, if $x < y$ then $\operatorname{pred}(x) < \operatorname{pred}(y)$.

WithTop.pred_le_pred theorem

(hxy : x ≤ y) : x.pred ≤ y.pred

Full source

@[gcongr] lemma pred_le_pred (hxy : x ≤ y) : x.pred ≤ y.pred := pred_mono hxy

Predecessor Function Preserves Order on Extended Type with Top

Informal description

For any elements $x, y$ in $\text{WithTop}\ \alpha$, if $x \leq y$, then the predecessor of $x$ is less than or equal to the predecessor of $y$.

WithTop.pred_lt_pred theorem

[NoMinOrder α] (hxy : x < y) : x.pred < y.pred

Full source

@[gcongr] lemma pred_lt_pred [NoMinOrder α] (hxy : x < y) : x.pred < y.pred := pred_strictMono hxy

Strict Monotonicity of Predecessor Function on $\text{WithTop}\ \alpha$

Informal description

Let $\alpha$ be a type with a strict order and no minimal element. For any elements $x, y$ in $\text{WithTop}\ \alpha$, if $x < y$, then the predecessor of $x$ is strictly less than the predecessor of $y$.

WithTop.pred_eq_top theorem

(a : WithTop α) : WithTop.pred a = ⊤ ↔ a = ⊤

Full source

@[simp]
theorem pred_eq_top (a : WithTop α) : WithTop.predWithTop.pred a = ⊤ ↔ a = ⊤ := by
  cases a
  · simp
  · simp only [WithTop.pred_coe, WithTop.coe_ne_top, iff_false]
    apply ne_of_lt
    by_contra! h
    have h₂ : _ = ⊤ := top_le_iff.mp (h.trans (Order.pred_le _))
    exact not_isMin_top (h₂ ▸ Order.min_of_le_pred (le_top.trans h))

Characterization of Predecessor of Top Element: $\text{pred}(a) = \top \leftrightarrow a = \top$

Informal description

For any element $a$ in $\text{WithTop}\ \alpha$, the predecessor of $a$ equals the top element $\top$ if and only if $a$ itself is the top element $\top$.