Ioc_insert_left

Mathlib.Order.Interval.Set.Basic

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

English

For a ≤ b, inserting the right endpoint into Ico(a, b) yields Icc(a, b): insert b (Ico a b) = Icc a b.

Русский

Для a ≤ b добавление правого конца в Ico(a, b) даёт Icc(a, b).

LaTeX

$$$$ \\mathrm{insert}\\; b\\; (Ico(a,b)) = Icc(a,b) \\quad\\text{if } a \\le b. $$$$

Lean4

@[simp]
theorem Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b := by rw [insert_eq, union_comm, Ioc_union_left h]

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

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

Разделы

Аффилиация

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