English
For any four points a,b,c,d in a Euclidean-type space, a form of Ptolemy inequality holds: dist(a,c) dist(b,d) ≤ dist(a,b) dist(c,d) + dist(b,c) dist(a,d).
Русский
Для любых четырех точек a,b,c,d в евклидовом пространстве выполняется неравенство, напоминающее Птолемея: dist(a,c) dist(b,d) ≤ dist(a,b) dist(c,d) + dist(b,c) dist(a,d).
LaTeX
$$$d(a,c)\, d(b,d) \le d(a,b)\, d(c,d) + d(b,c)\, d(a,d)$$$
Lean4
protected theorem inversion {α : Type*} {x c : P} {R : ℝ} {l : Filter α} {fc fx : α → P} {fR : α → ℝ}
(hc : Tendsto fc l (𝓝 c)) (hR : Tendsto fR l (𝓝 R)) (hx : Tendsto fx l (𝓝 x)) (hne : x ≠ c) :
Tendsto (fun a ↦ inversion (fc a) (fR a) (fx a)) l (𝓝 (inversion c R x)) :=
(((hR.div (hx.dist hc) <| dist_ne_zero.2 hne).pow 2).smul (hx.vsub hc)).vadd hc
