Iic_subset_Iio_union_Icc

Mathlib.Order.Interval.Set.LinearOrder

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

English

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

Русский

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

LaTeX

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

Lean4

theorem Iic_subset_Iio_union_Icc : Iic b ⊆ Iio a ∪ Icc a b := fun x hx =>
  (lt_or_ge x a).elim (fun hxa => Or.inl hxa) fun hxa => Or.inr ⟨hxa, hx⟩

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

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

Разделы

Аффилиация

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