forall₂_imp — Mathlib

English

If for all a and b, p a b implies q a b, then (for all a,b, p a b) implies (for all a,b, q a b).

Русский

Если для всех a,b выполняется p(a,b)→q(a,b), то если для всех a,b выполняется p(a,b), то для всех a,b выполняется q(a,b).

LaTeX

$$$(\\\\forall a\\\\,\\\\forall b, p(a,b)\\\\rightarrow q(a,b))\\\\rightarrow(\\\\forall a\\\\,\\\\forall b, p(a,b))\\\\rightarrow(\\\\forall a\\\\,\\\\forall b, q(a,b))$$$

Lean4

theorem forall₂_imp {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b → q a b) : (∀ a b, p a b) → ∀ a b, q a b :=
  forall_imp fun i ↦ forall_imp <| h i

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