nndist_lineMap_left — Mathlib

English

The distance between lineMap(p1,p2,c1) and lineMap(p1,p2,c2) equals |c1 − c2| times dist(p1,p2).

Русский

Расстояние между lineMap(p1,p2,c1) и lineMap(p1,p2,c2) равно |c1 − c2| умноженное на расстояние между p1 и p2.

LaTeX

$$$$ \mathrm{dist}(\text{lineMap}(p_1,p_2)(c_1), \text{lineMap}(p_1,p_2)(c_2)) = |c_1 - c_2| \cdot \mathrm{dist}(p_1,p_2). $$$$

Lean4

@[simp]
theorem nndist_lineMap_left (p₁ p₂ : P) (c : 𝕜) : nndist (lineMap p₁ p₂ c) p₁ = ‖c‖₊ * nndist p₁ p₂ :=
  NNReal.eq <| dist_lineMap_left _ _ _

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