one_le_dist_inr_inl — Mathlib

English

The distance between a left element and a right element across the glue is at least ε; this is the crossing bound used in glueDist.

Русский

Расстояние между элементами слева и справа через склейку не меньше ε; это пересечение границы используется в glueDist.

LaTeX

$$$ \varepsilon \le glueDist \Phi \Psi \varepsilon (\mathrm{Sum.inl} x)(\mathrm{Sum.inr} y). $$$

Lean4

theorem one_le_dist_inr_inl {x : X} {y : Y} : 1 ≤ Sum.dist (.inr y) (.inl x) := by rw [Sum.dist_comm];
  exact Sum.one_le_dist_inl_inr

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