forall' — Mathlib

English

A wrapper stating that forall over PProd is equivalent to forall over α and β, i.e., the same as PProd.forall.

Русский

Обобщение forall над PProd эквивалентно forall по компонентам α и β.

LaTeX

$$$\\forall p : PProd \\;α\\;β \\to Prop,\\; (\\forall x : PProd α β, p\,x) \\leftrightarrow (\\forall a : α, \\forall b : β, p\\langle a,b\\rangle).$$$

Lean4

theorem forall' {p : α → β → Prop} : (∀ x : PProd α β, p x.1 x.2) ↔ ∀ a b, p a b :=
  PProd.forall

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