Ioo_inter_Ioc_of_right_lt

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

If b2 < b1, then Ioo(a1, b1) ∩ Ioc(a2, b2) = Ioc(max(a1, a2), b2).

Русский

Если b2 < b1, то Ioo(a1, b1) ∩ Ioc(a2, b2) = Ioc(max(a1, a2), b2).

LaTeX

$$(b_2 < b_1) \\\\Rightarrow Ioo(a_1,b_1) \\\\cap Ioc(a_2,b_2) = Ioc(\\\\max(a_1,a_2), b_2)$$

Lean4

theorem Ioo_inter_Ioc_of_right_lt (h : b₂ < b₁) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂ := by
  rw [inter_comm, Ioc_inter_Ioo_of_left_lt h, max_comm]

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

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

Разделы

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

Аффилиация

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