dist_toLp_fst — Mathlib

English

The distance in the α-coordinate between (x1,0) and (x2,0) matches the distance between x1 and x2 in α: dist(toLp p (x1,0), toLp p (x2,0)) = dist(x1,x2).

Русский

Расстояние между левыми компонентами совпадает с расстоянием между x1 и x2 в α: dist(toLp p (x1,0), toLp p (x2,0)) = dist(x1,x2).

LaTeX

$$$\mathrm{dist}\bigl(toLp(p)(x_1,0), toLp(p)(x_2,0)\bigr) = \mathrm{dist}(x_1,x_2).$$$

Lean4

@[simp]
theorem dist_toLp_fst (x₁ x₂ : α) : dist (toLp p (x₁, (0 : β))) (toLp p (x₂, 0)) = dist x₁ x₂ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nndist_toLp_fst p α β x₁ x₂

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