English
A construction shows that a continuous map between normed spaces that preserves midpoints extends to a real-affine map.
Русский
Построение показывает, что непрерывное отображение между нормированными пространствами, сохраняющее середины, расширяется до действительного аффинного отображения.
LaTeX
$$$\text{AffineMap Real } P Q$ выполняется, если $f(\mathrm{midpoint}\; x\; y) = \mathrm{midpoint}\; (f x)\; (f y)$ и $f$ непрерывно.$$
Lean4
/-- A continuous map between two normed affine spaces is an affine map provided that
it sends midpoints to midpoints. -/
def ofMapMidpoint (f : P → Q) (h : ∀ x y, f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)) (hfc : Continuous f) :
P →ᵃ[ℝ] Q :=
let c := Classical.arbitrary P
AffineMap.mk' f
(↑((AddMonoidHom.ofMapMidpoint ℝ ℝ ((AffineEquiv.vaddConst ℝ (f <| c)).symm ∘ f ∘ AffineEquiv.vaddConst ℝ c)
(by simp) fun x y => by simp [h]).toRealLinearMap <|
by apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id]))
c fun p => by simp
