empty_promises

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.empty_promises

English

The empty computation promises every element of the type, i.e., for any a, empty α promises a.

Русский

Пустое вычисление обещает любой элемент типа, то есть для любого a, пустое α обещает a.

LaTeX

$$$\forall a,\ (\text{empty }\alpha) ~> a$$$

Lean4

theorem empty_promises (a : α) : empty α ~> a := fun _ h => absurd h (notMem_empty _)

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

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

Разделы

Аффилиация

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