imp — Mathlib

English

If every p-application implies q, then a triplewise p-l list also triplewise q.

Русский

Если для всех a,b,c выполнение p a b c ⇒ q a b c, тогда l.Triplewise p ⇒ l.Triplewise q.

LaTeX

$$$$ (h : \\forall {a b c}, p a b c \\Rightarrow q a b c) \\rightarrow (hl : l.Triplewise p) \\Rightarrow l.Triplewise q. $$$$

Lean4

theorem imp (h : ∀ {a b c}, p a b c → q a b c) (hl : l.Triplewise p) : l.Triplewise q := by
  induction hl with
  | nil => exact .nil
  | cons head tail ih => exact .cons (head.imp h) ih

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