Ico_inter_Ico

Mathlib.Order.Interval.Multiset

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

English

The intersection of Ico(a,b) and Ico(c,d) is Ico(max(a,c), min(b,d)).

Русский

Пересечение Ico(a,b) и Ico(c,d) равно Ico(max(a,c), min(b,d)).

LaTeX

$$$ Ico(a,b) \cap Ico(c,d) = Ico(\max(a,c), \min(b,d)) $$$

Lean4

theorem Ico_inter_Ico : Ico a b ∩ Ico c d = Ico (max a c) (min b d) := by
  rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]

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

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

Разделы

Аффилиация

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