English
If a map f: E → F sends 0 to 0 and sends midpoints to midpoints, then f is an additive monoid homomorphism.
Русский
Если отображение f сохраняет ноль и середины, то оно является гомоморфизмом моноида сложения.
LaTeX
$$$ (f(x+y) = f(x) + f(y)) \quad \text{for all } x,y \in E $$$
Lean4
/-- A map `f : E → F` sending zero to zero and midpoints to midpoints is an `AddMonoidHom`. -/
def ofMapMidpoint (f : E → F) (h0 : f 0 = 0) (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) : E →+ F
where
toFun := f
map_zero' := h0
map_add' x
y :=
calc
f (x + y) = f 0 + f (x + y) := by rw [h0, zero_add]
_ = midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) := (midpoint_add_self _ _ _).symm
_ = f (midpoint R x y) + f (midpoint R x y) := by rw [← hm, midpoint_zero_add]
_ = f x + f y := by rw [hm, midpoint_add_self]
