iSup_false

Mathlib.Order.CompleteLattice.Basic

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

English

If s is a function from False to α, the supremum over its domain equals the bottom element: iSup s = ⊥.

Русский

Если s: False → α, то верхняя грань iSup s равна нолю: iSup s = ⊥.

LaTeX

$$$\\\\bigvee_{x} s(x) = \\bot$$$

Lean4

theorem iSup_false {s : False → α} : iSup s = ⊥ := by simp

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

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

Разделы

Аффилиация

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