Iio_union_Icc_eq_Iic

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

For any a, b, [a, ∞) ⊆ [a,b] ∪ [b, ∞).

Русский

Для любых a, b, [a, ∞) ⊆ [a,b] ∪ [b, ∞).

LaTeX

$$$[a,\infty) \subseteq [a,b] \cup [b,\infty).$$

Lean4

@[simp]
theorem Iio_union_Icc_eq_Iic (h : a ≤ b) : Iio a ∪ Icc a b = Iic b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx => (le_of_lt hx).trans h) And.right) Iic_subset_Iio_union_Icc

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

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

Разделы

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

Аффилиация

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