not_terminates_empty

Mathlib.Data.Seq.Computation

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

English

¬ Terminates (empty α).

Русский

Не терминирует (пустое α).

LaTeX

$$$\lnot \mathrm{Terminates}(\empty(α))$$$

Lean4

theorem not_terminates_empty : ¬Terminates (empty α) := fun ⟨⟨a, h⟩⟩ => notMem_empty a h

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

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

Разделы

Аффилиация

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