uIcc_comm

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

The unordered interval is symmetric in its endpoints: [[a,b]] = [[b,a]].

Русский

Неупорядоченная интервал симметрична относительно концевых точек: [[a,b]] = [[b,a]].

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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