dist_le_of_mem_Icc_01 — Mathlib

English

If x and y lie in the interval [0,1], then the distance between x and y is at most 1.

Русский

Если x и y лежат в интервале [0,1], то расстояние между ними не превосходит 1.

LaTeX

$$$\\forall x, y \\in \\mathbb{R},\\ x \\in Icc(0,1) \\land y \\in Icc(0,1) \\Rightarrow \\operatorname{dist}(x,y) \\le 1$$$

Lean4

theorem dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 1) : dist x y ≤ 1 := by
  simpa only [sub_zero] using Real.dist_le_of_mem_Icc hx hy

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