eq_empty_of_not_terminates

Mathlib.Data.Seq.Computation

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

Lean4

theorem eq_empty_of_not_terminates {s} (H : ¬Terminates s) : s = empty α :=
  by
  apply Subtype.eq; funext n
  rcases h : s.val n; · rfl
  refine absurd ?_ H; exact ⟨⟨_, _, h.symm⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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