nonempty_uIcc

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

For any a,b in a lattice, the unordered interval [[a,b]] is nonempty.

Русский

Для любых a,b в решётке неупорядоченная интервал [[a,b]] непустой.

LaTeX

$$$$ [[a,b]].Nonempty. $$$$

Lean4

@[simp]
theorem nonempty_uIcc : [[a, b]].Nonempty :=
  nonempty_Icc.2 inf_le_sup

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

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

Разделы

Аффилиация

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