Ioc_union_Ioc_left

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_union_Ioc_left : Ioc a c ∪ Ioc b c = Ioc (min a b) c := by
  rw [Ioc_union_Ioc, max_self] <;> exact (min_le_right _ _).trans (le_max_right _ _)

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

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

Разделы

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

Аффилиация

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