Ico_inter_Ico

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

Ico a1 b1 ∩ Ico a2 b2 = Ico (a1 ⊔ a2) (b1 ⊓ b2).

Русский

Пересечение Ico(a1,b1) и Ico(a2,b2) равно Ico(max(a1,a2), min(b1,b2)).

LaTeX

$$$\mathrm{Ico}(a_1,b_1) \cap \mathrm{Ico}(a_2,b_2) = \mathrm{Ico}(\max(a_1,a_2), \min(b_1,b_2))$$$

Lean4

theorem Ico_inter_Ico : Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ici_inter_Iio.symm, Ici_inter_Ici.symm, Iio_inter_Iio.symm]; ac_rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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