English
Let E be a normed real vector space. If a,b ∈ ℝ satisfy a ≥ 0, b ≥ 0 and a + b = 1, then for any x,z ∈ E there exists y ∈ E with dist(x,y) = b dist(x,z) and dist(y,z) = a dist(x,z).
Русский
Пусть E — нормированное вещественное векторное пространство. Пусть a,b ∈ ℝ удовлетворяют a ≥ 0, b ≥ 0 и a + b = 1. Тогда для любых x,z ∈ E существует y ∈ E такое, что dist(x,y) = b dist(x,z) и dist(y,z) = a dist(x,z).
LaTeX
$$$$\forall x,z \in E\,\forall a,b \in \mathbb{R},\ a \ge 0,\ b \ge 0,\ a+b=1\;\Rightarrow\; \exists y \in E: \ dist(x,y)=b\,dist(x,z) \wedge dist(y,z)=a\,dist(x,z). $$$$
Lean4
theorem exists_dist_eq (x z : E) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z :=
by
use a • x + b • z
nth_rw 1 [← one_smul ℝ x]
nth_rw 4 [← one_smul ℝ z]
simp [dist_eq_norm, ← hab, add_smul, ← smul_sub, norm_smul_of_nonneg, ha, hb]
