antilipschitzWith_lineMap — Mathlib

English

For p1 ≠ p2 in a normed torsor, lineMap is antilipschitz with the inverse of the distance between p1 and p2 as the constant.

Русский

Для p1 ≠ p2 в нормированной торсоре отображение lineMap является антилипшицевым с константой, равной обратной мере расстояния между p1 и p2.

LaTeX

$$$\text{AntilipschitzWith} \bigl( (\mathrm{nndist}\; p_1\; p_2)^{-1} \bigr)\; ( (\mathrm{AffineMap.lineMap}\; p_1\; p_2) : 𝕜 \to Q)$$$

Lean4

theorem antilipschitzWith_lineMap {p₁ p₂ : Q} (h : p₁ ≠ p₂) :
    AntilipschitzWith (nndist p₁ p₂)⁻¹ (lineMap p₁ p₂ : 𝕜 → Q) :=
  AntilipschitzWith.of_le_mul_dist fun c₁ c₂ => by
    rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm, inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]

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