Ico_union_Ici'

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

If c ≤ b, then [a,b) ∪ [c, ∞) equals [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 Ico_union_Ici' (h₁ : c ≤ b) : Ico a b ∪ Ici c = Ici (min a c) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Ico, mem_Ici, min_le_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x < b := (lt_of_not_ge hc).trans_le h₁
    tauto

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

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

Разделы

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

Аффилиация

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