append_append_left_iff — Mathlib

English

Appending the same left factor preserves reductions: Red (L ++ L1) (L ++ L2) iff Red L1 L2.

Русский

При добавлении слева одного и того же множителя редукции сохраняются: Red (L ++ L1) (L ++ L2) эквивалентно Red L1 L2.

LaTeX

$$$Red(L \!++\! L_1, L \!++\! L_2) \iff Red(L_1, L_2)$$$

Lean4

@[to_additive]
theorem append_append_left_iff : ∀ L, Red (L ++ L₁) (L ++ L₂) ↔ Red L₁ L₂
  | [] => Iff.rfl
  | p :: L => by simp [append_append_left_iff L, cons_cons_iff]

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