uIcc_comm

Mathlib.Order.Interval.Finset.Basic

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

English

The upper interval is symmetric: [[a,b]] = [[b,a]].

Русский

Верхний интервал симметричен: [[a,b]] = [[b,a]].

LaTeX

$$[[a,b]] = [[b,a]]$$

Lean4

theorem uIcc_comm (a b : α) : [[a, b]] = [[b, a]] := by rw [uIcc, uIcc, inf_comm, sup_comm]

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

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

Разделы

Аффилиация

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