dist_toLp_snd — Mathlib

English

The edistance in α-component is preserved along the first coordinate: edist(toLp p (x1,0), toLp p (x2,0)) = edist(x1,x2).

Русский

Едистанция в α-компоненте сохраняется вдоль первой координаты: edist(toLp p (x1,0), toLp p (x2,0)) = edist(x1,x2).

LaTeX

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

Lean4

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

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