opow_mul_add_lt_opow_succ — Mathlib

English

For b,u,w with v >? and w < b^u, then b^u · succ v > b^u · v + w.

Русский

Пусть b,u,w такие, что w < b^u; тогда b^u · succ v > b^u · v + w.

LaTeX

$$$\forall b,u,w,v \in \mathrm{Ordinal},\ w < b^{u} \Rightarrow b^{u} \cdot \operatorname{succ} v > b^{u} \cdot v + w$$$

Lean4

@[deprecated opow_mul_add_lt_opow_succ (since := "2025-08-27")]
theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < b ^ u) : b ^ u * v + w < b ^ succ u :=
  opow_mul_add_lt_opow hvb hw (lt_succ u)

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