uIcc_of_lt

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

If a < b, then uIcc(a,b) = Icc(a,b).

Русский

Если a < b, то uIcc(a,b) = Icc(a,b).

LaTeX

$$$$ \text{If } a < b, \ \ [[a,b]] = Icc(a,b). $$$$

Lean4

theorem uIcc_of_lt (h : a < b) : [[a, b]] = Icc a b :=
  uIcc_of_le h.le

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

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

Разделы

Аффилиация

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