dist_midpoint_midpoint_le — Mathlib

English

If a map f between normed spaces sends midpoints to midpoints and is continuous, it defines an affine map between the spaces.

Русский

Если отображение f между нормированными пространствами отправляет середины на середины и непрерывно, то оно задаёт аффинное отображение между пространствами.

LaTeX

$$$f\colon P\to Q$ с условием\forall x,y, f( \mathrm{midpoint}\; x\; y) = \mathrm{midpoint}\; (f x)\; (f y) \Rightarrow f\in\mathrm{AffineMap}\\text{Real}$$$

Lean4

theorem dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
    dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 := by
  simpa using dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄

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