Icc_min_max

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.Icc_min_max

English

For any a,b, the Icc between min(a,b) and max(a,b) equals the uIcc between a and b.

Русский

Для любых a, b интервалы Icc(min(a,b), max(a,b)) равны uIcc(a,b).

LaTeX

$$$Icc(\min(a,b), \max(a,b)) = [[a, b]]$$$

Lean4

theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
  rfl

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

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

Разделы

Аффилиация

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