forall' — Mathlib

English

The universal quantification over a product is equivalent to a universal quantification over each coordinate: (∀ x : α×β, p x.1 x.2) ↔ ∀ a b, p a b.

Русский

Универсальная квантор над произведением равносилен по координатам: (∀ x : α×β, p x.1 x.2) ↔ ∀ a b, p a b.

LaTeX

$$$$ \\forall x : \\alpha \\times \\beta,\\; p(x.1,x.2) \\iff \\forall a,b,\\; p(a,b) $$$$

Lean4

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

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