append_overlap — Mathlib

English

If (L1 ++ L2) and (L2 ++ L3) are reduced and L2 is nonempty, then (L1 ++ L2 ++ L3) is reduced.

Русский

Если (L1 ++ L2) и (L2 ++ L3) редуцированы, и L2 непусто, то (L1 ++ L2 ++ L3) редуцировано.

LaTeX

$$$\operatorname{IsReduced}(L_1 ++ L_2) \rightarrow \operatorname{IsReduced}(L_2 ++ L_3) \rightarrow L_2 \neq \emptyset \rightarrow \operatorname{IsReduced}(L_1 ++ L_2 ++ L_3).$$$

Lean4

@[to_additive]
theorem append_overlap {L₁ L₂ L₃ : List (α × Bool)} (h₁ : IsReduced (L₁ ++ L₂)) (h₂ : IsReduced (L₂ ++ L₃))
    (hn : L₂ ≠ []) : IsReduced (L₁ ++ L₂ ++ L₃) :=
  IsChain.append_overlap h₁ h₂ hn

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