English
Let f: R → Γ0 be a function satisfying f(0) = ⊤, f(1) = 0, and the usual additivity inequalities f(x + y) ≥ min(f(x), f(y)) together with f(xy) = f(x) + f(y). Then the additive valuation built from f via AddValuation.of has the property that it agrees with f on every r: (AddValuation.of f h0 h1 hadd hmul)(r) = f(r) for all r.
Русский
Пусть f: R → Γ0 удовлетворяет f(0) = ⊤, f(1) = 0, неравенствам аддитивности f(x + y) ≥ min(f(x), f(y)) и равенству f(xy) = f(x) + f(y). Тогда аддитивная оценка, построенная из f функцией AddValuation.of, совпадает с f на каждом элементе r: (AddValuation.of f h0 h1 hadd hmul)(r) = f(r) для всех r.
LaTeX
$$$$ \forall r,\ (\mathrm{of}\ f\ h_0\ h_1\ hadd\ hmul)\ r = f(r). $$$$
Lean4
@[simp]
theorem of_apply : (of f h0 h1 hadd hmul) r = f r :=
rfl
