Ioo_union_Ioi'

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

Iio a ⊊ Iio b iff a < b.

Русский

Iio a ⊊ Iio b тогда и только тогда a < b.

LaTeX

$$$ Iio(a) \subset Iio(b) \iff a < b $$$

Lean4

theorem Ioo_union_Ioi' (h₁ : c < b) : Ioo a b ∪ Ioi c = Ioi (min a c) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Ioo, mem_Ioi, min_lt_iff]
  by_cases hc : c < x
  · tauto
  · have hxb : x < b := (le_of_not_gt hc).trans_lt h₁
    tauto

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

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

Разделы

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

Аффилиация

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