edist_toLp_fst — Mathlib

English

A reiteration: edist between two first-coordinate elements in WithLp p (α × β) equals the edist in α.

Русский

Повторение: edist между двумя элементами с первой координатой в WithLp p (α × β) равно edist в α.

LaTeX

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

Lean4

@[simp]
theorem edist_toLp_fst (x₁ x₂ : α) : edist (toLp p (x₁, (0 : β))) (toLp p (x₂, 0)) = edist x₁ x₂ := by
  simp only [edist_nndist, nndist_toLp_fst p α β x₁ x₂]

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