uIcc_subset_uIcc_union_uIcc

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.uIcc_subset_uIcc_union_uIcc

← MathLib Explorer

English

Between a and c, the interval [[a,c]] is contained in the union [[a,b]] ∪ [[b,c]].

Русский

Между a и 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]] :=
  coe_subset.1 <| by
    push_cast
    exact Set.uIcc_subset_uIcc_union_uIcc

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru