edist_toLp_snd — Mathlib

English

Similarly, edist between two second-coordinate elements equals the edist in β: edist(toLp p ((0,y1)), toLp p ((0,y2))) = edist(y1,y2).

Русский

Аналогично: edist между двумя вторыми координатами равен edist между y1 и y2 в β.

LaTeX

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

Lean4

@[simp]
theorem edist_toLp_snd (y₁ y₂ : β) : edist (toLp p ((0 : α), y₁)) (toLp p (0, y₂)) = edist y₁ y₂ := by
  simp only [edist_nndist, nndist_toLp_snd p α β y₁ y₂]

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