orElse_empty — Mathlib

English

c <|> empty α equals c.

Русский

c <|> empty α эквивалентно c.

LaTeX

$$$ c \\mathbf{<|>} \\ \operatorname{empty} \alpha = c$$$

Lean4

@[simp]
theorem orElse_empty (c : Computation α) : (c <|> empty α) = c :=
  by
  apply eq_of_bisim (fun c₁ c₂ => (c₂ <|> empty α) = 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]

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