Ico_union_Ici

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

If c ≤ max(a,b), then [a,b) ∪ [c, ∞) equals [min(a,c), ∞).

Русский

Если c ≤ max(a,b), то [a,b) ∪ [c, ∞) равно [min(a,c), ∞).

LaTeX

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

Lean4

theorem Ico_union_Ici (h : c ≤ max a b) : Ico a b ∪ Ici c = Ici (min a c) :=
  by
  rcases le_total a b with hab | hab
  · simp only [hab, sup_of_le_right] at h; exact Ico_union_Ici' h
  · simp_all

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

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

Разделы

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

Аффилиация

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