Iic_union_Ioc'

Mathlib.Order.Interval.Set.LinearOrder

URI: https://scilib.ai/kg/mathlib#Set.Iic_union_Ioc'

← MathLib Explorer

English

If c < b, then [−∞, b] ∪ (c,d] = [−∞, max(b,d)].

Русский

Если c < b, то [−∞, b] ∪ (c,d] = [−∞, max(b,d)].

LaTeX

$$$(-\infty, b] \cup (c,d] = (-\infty, \max(b,d)] \quad (c < b).$$

Lean4

theorem Iic_union_Ioc' (h₁ : c < b) : Iic b ∪ Ioc c d = Iic (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Iic, mem_Ioc, le_max_iff]
  by_cases hc : c < x
  · tauto
  · have hxb : x ≤ b := (le_of_not_gt hc).trans h₁.le
    tauto

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

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

Разделы

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

Аффилиация

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