lipschitzWith_lineMap — 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 как функция по параметру Lipschitz с константой, равной расстоянию между p1 и p2.

LaTeX

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

Lean4

theorem lipschitzWith_lineMap (p₁ p₂ : P) : LipschitzWith (nndist p₁ p₂) (lineMap p₁ p₂ : 𝕜 → P) :=
  LipschitzWith.of_dist_le_mul fun c₁ c₂ => ((dist_lineMap_lineMap p₁ p₂ c₁ c₂).trans (mul_comm _ _)).le

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