Ioc_diff_Iic

Mathlib.Order.Interval.Set.LinearOrder

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

English

If b1 < b2, then Ioc(a1, b1) ∩ Ioo(a2, b2) = Ioc(max(a1, a2), b1).

Русский

Если b1 < b2, то Ioc(a1, b1) ∩ Ioo(a2, b2) = Ioc(max(a1, a2), b1).

LaTeX

$$(b_1 < b_2) \\\\Rightarrow Ioc(a_1,b_1) \\\\cap Ioo(a_2,b_2) = Ioc(\\\\max(a_1,a_2), b_1)$$

Lean4

@[simp]
theorem Ioc_diff_Iic : Ioc a b \ Iic c = Ioc (max a c) b := by rw [diff_eq, compl_Iic, Ioc_inter_Ioi]

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

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

Разделы

Аффилиация

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