Iio_eq

Mathlib.Order.Cover

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

English

If a ⋖ b, then Iio(b) = Iic(a).

Русский

Если a ⋖ b, то Iio(b) = Iic(a).

LaTeX

$$Iio(b) = Iic(a)$$

Lean4

theorem Iio_eq (h : a ⋖ b) : Iio b = Iic a := by rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]

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

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

Разделы

Аффилиация

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