Ioc_inter_Ioi

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

The intersection of Ioc a b and Ioi c equals Ioc (max(a, c)) b.

Русский

Пересечение Ioc(a,b) и Ioi(c) равняется Ioc(max(a,c), b).

LaTeX

$$$Ioc(a,b) \\\\cap Ioi(c) = Ioc(\\\\max(a,c)) b$$$

Lean4

@[simp]
theorem Ioc_inter_Ioi : Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b := by
  rw [← Ioi_inter_Iic, inter_assoc, inter_comm, inter_assoc, Ioi_inter_Ioi, inter_comm, Ioi_inter_Iic, sup_comm]

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

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

Разделы

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

Аффилиация

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