Ico_inter_Iio

Mathlib.Order.Interval.Set.LinearOrder

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ico_inter_Iio : Ico a b ∩ Iio c = Ico a (min b c) :=
  ext <| by simp +contextual [iff_def]

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

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

Разделы

Аффилиация

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