Iic_union_Ioo_eq_Iio

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

Let a < b. Then Iic(a) ∪ Ioo(a,b) = Iio(b).

Русский

Пусть a < b. Тогда Iic(a) ∪ Ioo(a,b) = Iio(b).

LaTeX

$$$ a < b \implies Iic(a) \cup Ioo(a,b) = Iio(b). $$$

Lean4

@[simp]
theorem Iic_union_Ioo_eq_Iio (h : a < b) : Iic a ∪ Ioo a b = Iio b :=
  Subset.antisymm (fun _ hx => hx.elim (fun hx' => lt_of_le_of_lt hx' h) And.right) Iio_subset_Iic_union_Ioo

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

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

Разделы

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

Аффилиация

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