mk'_right₀ — Mathlib

English

The right component of a tape built as Tape.mk' L R is simply R: (Tape.mk' L R).right₀ = R.

Русский

Правый компонент ленты, собранной как Tape.mk' L R, равен R: (Tape.mk' L R).right₀ = R.

LaTeX

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

Lean4

@[simp]
theorem mk'_right₀ {Γ} [Inhabited Γ] (L R : ListBlank Γ) : (Tape.mk' L R).right₀ = R :=
  ListBlank.cons_head_tail _

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