imp — Mathlib

English

If for all a,b the relation R a b implies S a b, then Forall₂ R l1 l2 implies Forall₂ S l1 l2 for any lists l1, l2.

Русский

Если для всех a,b отношение R a b подразумевает S a b, то если Forall₂ R l1 l2, то Forall₂ S l1 l2 для любых списков l1,l2.

LaTeX

$$$$ (\\forall a,b,\\ R\\ a\\ b \\to S\\ a\\ b) \\Rightarrow (\\forall l_1\\ l_2,\\ \\mathrm{Forall₂}\\ R\\ l_1\\ l_2 \\to \\mathrm{Forall₂}\\ S\\ l_1\\ l_2). $$$$

Lean4

theorem imp (H : ∀ a b, R a b → S a b) {l₁ l₂} (h : Forall₂ R l₁ l₂) : Forall₂ S l₁ l₂ := by
  induction h <;> constructor <;> solve_by_elim

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