iSup_true

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iSup_true

English

For any s: True → α, the supremum equals the value at the unique element of True: iSup s = s(trivial).

Русский

Для любой s: True → α верхняя граница равна значению в единственном элементе True: iSup s = s(тривиальное).

LaTeX

$$$\\\\bigvee_{x} s(x) = s(\\\\mathrm{trivial})$$$

Lean4

theorem iSup_true {s : True → α} : iSup s = s trivial :=
  iSup_pos trivial

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

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

Разделы

Аффилиация

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