Ioc_union_Ioc_symm

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_union_Ioc_symm : Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b) :=
  by
  rw [max_comm]
  apply Ioc_union_Ioc <;> rw [max_comm] <;> exact min_le_max

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

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

Разделы

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

Аффилиация

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