empty_orElse

Mathlib.Data.Seq.Computation

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

← MathLib Explorer

English

empty α <|> c = c.

Русский

empty α <|> c = c.

LaTeX

$$$ (\text{empty } \alpha) \\mathbf{<|>} \\ c = c$$$

Lean4

@[simp]
theorem empty_orElse (c) : (empty α <|> c) = c :=
  by
  apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl
  intro s' s h; rw [← h]
  induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

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

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

Разделы

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

Аффилиация

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