append_right — Mathlib

English

For any L1, L2, L3, Step L1 L2 implies Step (L1 ++ L3) (L2 ++ L3).

Русский

Для любых L1, L2, L3 из Step L1 L2 следует Step (L1 ++ L3) (L2 ++ L3).

LaTeX

$$$ \\forall L_1 L_2 L_3,\\; \\mathrm{Step}(L_1,L_2) \\Rightarrow \\mathrm{Step}(L_1 \\,+\\!\\,+ L_3,\\; L_2 \\,+\\!\\,+ L_3).$$$

Lean4

@[to_additive]
theorem append_right : ∀ {L₁ L₂ L₃ : List (α × Bool)}, Step L₁ L₂ → Step (L₁ ++ L₃) (L₂ ++ L₃)
  | _, _, _, Red.Step.not => by simp

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