mk'_left_right₀ — Mathlib

English

A tape built from L and R is equal to the original tape: Tape.mk' L R = T when L, R are the left/right parts of T.

Русский

Лента, построенная из L и R, равна исходной ленте: Tape.mk' L R = T.

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)], Tape.mk' (L) (R) = T$$$

Lean4

@[simp]
theorem mk'_left_right₀ {Γ} [Inhabited Γ] (T : Tape Γ) : Tape.mk' T.left T.right₀ = T := by
  simp only [Tape.right₀, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons]

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