Ioc_union_Ioc_right

Mathlib.Order.Interval.Set.LinearOrder

URI: https://scilib.ai/kg/mathlib#Set.Ioc_union_Ioc_right

← MathLib Explorer

English

Ioc a b ∪ Ioc a c = Ioc a (max b c).

Русский

Ioc(a,b) ∪ Ioc(a,c) = Ioc(a, max(b,c)).

LaTeX

$$$Ioc a b \\cup Ioc a c = Ioc a (\\\\max b c)$$$

Lean4

@[simp]
theorem Ioc_union_Ioc_right : Ioc a b ∪ Ioc a c = Ioc a (max b c) := by
  rw [Ioc_union_Ioc, min_self] <;> exact (min_le_left _ _).trans (le_max_left _ _)

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

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

Разделы

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

Аффилиация

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