abs_sub_le_of_uIcc_subset_uIcc — Mathlib

English

If a subinterval [c,d] is contained in [a,b], then the length of [c,d] is at most the length of [a,b].

Русский

Если подинтервал [c,d] содержится в [a,b], то его длина не превышает длину [a,b].

LaTeX

$$$[[c,d]] \subseteq [[a,b]] \Rightarrow |d - c| \le |b - a|$$

Lean4

/-- If `[c, d]` is a subinterval of `[a, b]`, then the distance between `c` and `d` is less than or
equal to that of `a` and `b` -/
theorem abs_sub_le_of_uIcc_subset_uIcc (h : [[c, d]] ⊆ [[a, b]]) : |d - c| ≤ |b - a| :=
  by
  rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]
  rw [uIcc_subset_uIcc_iff_le] at h
  exact sub_le_sub h.2 h.1

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