forall_append — Mathlib

English

Forall p holds on the concatenation xs ++ ys if and only if it holds on xs and on ys separately.

Русский

Forall p на xs ++ ys эквивалентно Forall p на xs и на ys поотдельности.

LaTeX

$$$ \\forall \\{xs,ys : List\\, \\alpha\\},\\ Forall\\ p\\ (xs++ys)\\ \\Leftrightarrow\\ (Forall\\ p\\ xs) \\land (Forall\\ p\\ ys) $$$

Lean4

@[simp]
theorem forall_append {p : α → Prop} : ∀ {xs ys : List α}, Forall p (xs ++ ys) ↔ Forall p xs ∧ Forall p ys
  | [] => by simp
  | _ :: _ => by simp [forall_append, and_assoc]

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