opow_mul_add_lt_opow — Mathlib

English

If v < b, w < b^u, and u < x, then b^u · v + w < b^x.

Русский

Если v < b, w < b^u и u < x, то b^u · v + w < b^x.

LaTeX

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

Lean4

theorem opow_mul_add_lt_opow {b u v w x : Ordinal} (hv : v < b) (hw : w < b ^ u) (hu : u < x) : b ^ u * v + w < b ^ x :=
  by
  apply (opow_mul_add_lt_opow_mul hw hv).trans_le
  rw [← opow_succ]
  exact opow_le_opow_right hv.pos (succ_le_of_lt hu)

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