log — Mathlib

English

For b,u,v,w,x with v < b, w < b^u and u < x, we have b^u · v + w < b^x.

Русский

Пусть b,u,v,w,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

/-- The ordinal logarithm is the solution `u` to the equation `x = b ^ u * v + w` where `v < b` and
`w < b ^ u`. -/
@[pp_nodot]
def log (b : Ordinal) (x : Ordinal) : Ordinal :=
  if 1 < b then pred (sInf {o | x < b ^ o}) else 0

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