Ioc_eq

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#CovBy.Ioc_eq

English

If a ⋖ b, then Ioc(a,b) = {b}.

Русский

Если a ⋖ b, то Ioc(a,b) = {b}.

LaTeX

$$Ioc(a,b) = \{ b \}$$

Lean4

theorem Ioc_eq (h : a ⋖ b) : Ioc a b = { b } := by rw [← Ioo_union_right h.lt, h.Ioo_eq, empty_union]

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

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

Разделы

Аффилиация

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