kerase_append_right — Mathlib

English

If a ∉ l1.keys, then kerase a (l1 ++ l2) = l1 ++ kerase a l2. Erasing a from the right part does not affect the left block.

Русский

Если a ∉ l1.keys, то kerase a (l1 ++ l2) = l1 ++ kerase a l2.

LaTeX

$$∀ {l1 l2 : List (Σ β)}, a ∉ l1.keys → kerase a (l1 ++ l2) = l1 ++ kerase a l2$$

Lean4

theorem kerase_append_right {a} : ∀ {l₁ l₂ : List (Sigma β)}, a ∉ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
  | [], _, _ => rfl
  | _ :: l₁, l₂, h => by
    simp only [keys_cons, mem_cons, not_or] at h
    simp [h.1, kerase_append_right h.2]

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