Icc_union_Ici'

Mathlib.Order.Interval.Set.LinearOrder

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

← 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 Icc_union_Ici' (h₁ : c ≤ b) : Icc a b ∪ Ici c = Ici (min a c) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Icc, mem_Ici, min_le_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
    tauto

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

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

Разделы

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

Аффилиация

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