dist_center_homothety — Mathlib

English

The line map p1 p2 as a function of the parameter is Lipschitz with constant equal to the distance between p1 and p2.

Русский

Линия отображения p1, p2 как функция по параметру липшицова с константой, равной расстоянию между p1 и p2.

LaTeX

$$$$ \text{LipschitzWith}( \mathrm{dist}(p_1,p_2), \ lineMap(p_1,p_2) : \mathbb{k} \to P ). $$$$

Lean4

@[simp]
theorem dist_center_homothety (p₁ p₂ : P) (c : 𝕜) : dist p₁ (homothety p₁ c p₂) = ‖c‖ * dist p₁ p₂ := by
  simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]

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