Ioc_inter_Ioc

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

Ioc a1 b1 ∩ Ioc a2 b2 = Ioc (a1 ⊔ a2) (b1 ⊓ b2).

Русский

Пересечение Ioc(a1,b1) и Ioc(a2,b2) равно Ioc(max(a1,a2), min(b1,b2)).

LaTeX

$$$\mathrm{Ioc}(a_1,b_1) \cap \mathrm{Ioc}(a_2,b_2) = \mathrm{Ioc}(\max(a_1,a_2), \min(b_1,b_2))$$$

Lean4

theorem Ioc_inter_Ioc : Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ioi_inter_Iic.symm, Ioi_inter_Ioi.symm, Iic_inter_Iic.symm]; ac_rfl

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

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

Разделы

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

Аффилиация

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