opow_mul_add_pos — Mathlib

English

If b ≠ 0 and v ≠ 0, then for any u,w, 0 < b^u · v + w.

Русский

Если b ≠ 0 и v ≠ 0, то для любых u,w выполняется 0 < b^u · v + w.

LaTeX

$$$\forall b,v,u,w \in \mathrm{Ordinal},\ b \neq 0 \Rightarrow v \neq 0 \Rightarrow 0 < b^{u} \cdot v + w$$$

Lean4

theorem opow_mul_add_pos {b v : Ordinal} (hb : b ≠ 0) (u : Ordinal) (hv : v ≠ 0) (w : Ordinal) : 0 < b ^ u * v + w :=
  (opow_pos u <| Ordinal.pos_iff_ne_zero.2 hb).trans_le <|
    (le_mul_left _ <| Ordinal.pos_iff_ne_zero.2 hv).trans <| le_add_right _ _

Похожие утверждения