dist_ne — Mathlib

English

If two points lie in different fibers, their distance equals the sum of their distances to the respective basepoints plus 1 between the basepoints.

Русский

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

LaTeX

$$$\forall i\neq j, x\in E_i, y\in E_j,\; \mathrm{dist}(\langle i,x\rangle,\langle j,y\rangle) = \mathrm{dist}_i(x,b_i) + 1 + \mathrm{dist}_j(b_j,y)$$$

Lean4

@[simp]
theorem dist_ne {i j : ι} (h : i ≠ j) (x : E i) (y : E j) :
    dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ = dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨y⟩) y :=
  dif_neg h

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