flatten_equiv — Mathlib

English

If c is a computation containing s, then flatten c is equivalent to s.

Русский

Если вычисление c содержит s, то flatten c эквивалентно s.

LaTeX

$$$\forall c:\mathrm{Computation}(\mathrm{WSeq}(\alpha)),\ s\in c \Rightarrow \mathrm{flatten}(c) \sim_W s$$$

Lean4

theorem flatten_equiv {c : Computation (WSeq α)} {s} (h : s ∈ c) : flatten c ~ʷ s :=
  by
  apply Computation.memRecOn h
  · simp [Equiv.refl]
  · intro s'
    apply Equiv.trans
    simp [think_equiv]

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