edist_mk_mk — Mathlib

English

The extended distance on a subtype is the restriction of the original distance: for x,y in α with hx,hy, edist((x,hx))((y,hy)) = edist(x,y).

Русский

Расстояние на подтипе — это ограничение исходного расстояния: для x,y в α с hx,hy выполняется edist((x,hx))((y,hy)) = edist(x,y).

LaTeX

$$$\operatorname{edist}((x,\,hx)),(y,\,hy)) = \operatorname{edist}(x,y).$$$

Lean4

/-- The extended pseudodistance on a subtype of a pseudoemetric space is the restriction of
the original pseudodistance, by definition. -/
@[simp]
theorem edist_mk_mk {p : α → Prop} {x y : α} (hx : p x) (hy : p y) : edist (⟨x, hx⟩ : Subtype p) ⟨y, hy⟩ = edist x y :=
  rfl

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