nndist_left_lineMap — Mathlib

English

The nonnegative distance between lineMap outputs is the product of the distance in parameter and the base distance.

Русский

Нормированное расстояние между значениями lineMap равняется произведению расстояния между аргументами и базового расстояния.

LaTeX

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

Lean4

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

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