Ioi_eq

Mathlib.Order.Cover

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

English

If a ⋖ b, then Ioi(a) = Ici(b).

Русский

Если a ⋖ b, то Ioi(a) = Ici(b).

LaTeX

$$Ioi(a) = \Iverson{b}{ }$$

Lean4

theorem Ioi_eq (h : a ⋖ b) : Ioi a = Ici b := by rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]

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

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

Разделы

Аффилиация

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