one_le_dist_of_ne — Mathlib

English

If two points lie in different fibers, then 1 ≤ dist((i,x),(j,y)).

Русский

Если точки лежат в разных фибрах, то 1 ≤ dist((i,x),(j,y)).

LaTeX

$$$\forall i\neq j, x\in E_i, y\in E_j,\; 1 \le \mathrm{dist}(\langle i,x\rangle,\langle j,y\rangle)$$$

Lean4

theorem one_le_dist_of_ne {i j : ι} (h : i ≠ j) (x : E i) (y : E j) : 1 ≤ dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ :=
  by
  rw [Sigma.dist_ne h x y]
  linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]

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