append_append — Mathlib

English

If L1 reduces to L3 and L2 reduces to L4, then the concatenation L1 ++ L2 reduces to L3 ++ L4.

Русский

Если L1 редуцируется до L3 и L2 до L4, то конкатенация L1 ++ L2 редуцируется до L3 ++ L4.

LaTeX

$$$Red(L_1, L_3) \land Red(L_2, L_4) \Rightarrow Red(L_1 ++ L_2, L_3 ++ L_4)$$$

Lean4

@[to_additive]
theorem append_append (h₁ : Red L₁ L₃) (h₂ : Red L₂ L₄) : Red (L₁ ++ L₂) (L₃ ++ L₄) :=
  (h₁.lift (fun L => L ++ L₂) fun _ _ => Step.append_right).trans ((append_append_left_iff _).2 h₂)

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