uIcc_subset_uIcc_union_uIcc — Mathlib

English

For any a,b,c, the unordered closed interval between a and c is contained in the union of the unordered closed intervals between a and b and between b and c.

Русский

Для любых a, b, c карка неупорядоченного замкнутого интервала между a и c содержится в объединении неупорядоченных замкнутых интервалов между a и b и между b и c.

LaTeX

$$$ [[a,c]] \\subseteq [[a,b]] \\cup [[b,c]] $$$

Lean4

/-- A sort of triangle inequality. -/
theorem uIcc_subset_uIcc_union_uIcc : [[a, c]] ⊆ [[a, b]] ∪ [[b, c]] := fun x =>
  by
  simp only [mem_uIcc, mem_union]
  rcases le_total x b with h2 | h2 <;> tauto

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