dist_same — Mathlib

English

If two points lie in the same fiber, their distance in the disjoint union equals the distance inside that fiber.

Русский

Если две точки лежат в одной и той же фибре, расстояние между ними в дизъюнктивном объединении равно расстоянию внутри этой фибры.

LaTeX

$$$\forall i\, \forall x,y \in E_i,\; \mathrm{dist}(\langle i,x\rangle,\langle i,y\rangle) = \mathrm{dist}_i(x,y)$$$

Lean4

@[simp]
theorem dist_same (i : ι) (x y : E i) : dist (Sigma.mk i x) ⟨i, y⟩ = dist x y := by simp [Dist.dist, Sigma.dist]

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