forall — Mathlib

English

A simp lemma: a universal statement over PProd α β is equivalent to a universal statement over α and β separately.

Русский

Лемма-упрощение: всеобщее утверждение над PProd α β эквивалентно всеобщему утверждению по каждому из α и β по отдельности.

LaTeX

$$$\\bigl(\\forall x : PProd \\;α\\;β,\\; p\\,x\\bigr) \\iff \\bigl(\\forall a : α,\\; \\forall b : β,\\; p\\langle a,b\\rangle\\bigr).$$$

Lean4

@[simp]
theorem «forall» {p : PProd α β → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ :=
  ⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩

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