coe_ofMapMidpoint — Mathlib

English

The underlying function of the constructed AddMonoidHom ofMapMidpoint equals the original map f; i.e., its value on any x is f(x).

Русский

Предел функции из построенного AddMonoidHom.ofMapMidpoint совпадает с исходной функцией f: ∀x, (ofMapMidpoint ... f ...)(x) = f(x).

LaTeX

$$$ \forall x,\ \big(\mathrm{ofMapMidpoint}_{R,R'} f\ h0\ hm\big)(x) = f(x) $$$

Lean4

@[simp]
theorem coe_ofMapMidpoint (f : E → F) (h0 : f 0 = 0) (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) :
    ⇑(ofMapMidpoint R R' f h0 hm) = f :=
  rfl

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