Ioo_union_both

Mathlib.Order.Interval.Set.Basic

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

← MathLib Explorer

English

If a ≤ b, then Ioo(a, b) ∪ {a, b} = Icc(a, b).

Русский

Если a ≤ b, то Ioo(a,b) ∪ {a, b} = Icc(a,b).

LaTeX

$$$$ Ioo(a,b) \\cup \\{a,b\\} = Icc(a,b) $$$$

Lean4

theorem Ioo_union_both (h : a ≤ b) : Ioo a b ∪ { a, b } = Icc a b :=
  by
  have : (Icc a b \ { a, b }) ∪ { a, b } = Icc a b :=
    diff_union_of_subset fun
      | x, .inl rfl => left_mem_Icc.mpr h
      | x, .inr rfl => right_mem_Icc.mpr h
  rw [← this, Icc_diff_both]

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

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

Разделы

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

Аффилиация

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