Ioc_union_Ioi'

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

If c ≤ b, then (a,b] ∪ (c, ∞) = (min(a,c), ∞).

Русский

Если c ≤ b, то (a,b] ∪ (c, ∞) = (min(a,c), ∞).

LaTeX

$$$(a,b] \cup (c,\infty) = (\min(a,c), \infty) \quad (c \le b).$$

Lean4

theorem Ioc_union_Ioi' (h₁ : c ≤ b) : Ioc a b ∪ Ioi c = Ioi (min a c) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Ioc, mem_Ioi, min_lt_iff]
  by_cases hc : c < x
  · tauto
  · have hxb : x ≤ b := (le_of_not_gt hc).trans h₁
    tauto

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

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

Разделы

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

Аффилиация

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