imp — Mathlib

English

If p implies q for every element, then Forall p l implies Forall q l.

Русский

Если для каждого элемента выполняется p x → q x, то If Forall p l, то Forall q l.

LaTeX

$$$ (\\forall x,\\ p x \\to q x) \\Rightarrow (\\forall {l : List\\, \\alpha},\\ Forall\\ p\\ l \\to Forall\\ q\\ l) $$$

Lean4

theorem imp (h : ∀ x, p x → q x) : ∀ {l : List α}, Forall p l → Forall q l
  | [] => id
  | x :: l => by
    simp only [forall_cons, and_imp]
    rw [← and_imp]
    exact And.imp (h x) (Forall.imp h)

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