English
If the distances satisfy a pair of linear relations with a ratio r, then the middle point lies on the affine line between the endpoints.
Русский
Если расстояния удовлетворяют паре линейных соотношений с коэффициентом r, то середина лежит на аффной прямой между концами.
LaTeX
$$$\forall x,y,z,\; dist(x,y)=r\,dist(x,z) \land dist(y,z)=(1-r)\,dist(x,z) \Rightarrow y = \mathrm{lineMap}(x,z,r)$$$
Lean4
theorem dist_lt_max_dist (p : P) {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : dist p₂ p < max (dist p₁ p) (dist p₃ p) :=
by
have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p := by simpa using h.left_ne_right
rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment, Set.mem_insert_iff,
Set.mem_insert_iff] at h
rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
· rw [vsub_left_cancel_iff] at h
exact False.elim (hp₂p₁ h)
· rw [vsub_left_cancel_iff] at h
exact False.elim (hp₂p₃ h)
· rw [openSegment_eq_image, Set.mem_image] at h
rcases h with ⟨r, ⟨hr0, hr1⟩, hr⟩
simp_rw [@dist_eq_norm_vsub V, ← hr]
exact norm_combo_lt_of_ne (le_max_left _ _) (le_max_right _ _) hp₁p₃ (sub_pos.2 hr1) hr0 (by abel)
