Ioo_inter_Ioc_of_left_le

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioo_inter_Ioc_of_left_le (h : b₁ ≤ b₂) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁ := by
  rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]

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

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

Разделы

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

Аффилиация

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