forall — Mathlib

English

A proposition holds for all PSigma elements iff it holds for all pairs (a,b).

Русский

Лемма forall для PSigma: свойство выполняется на всех элементах PSigma тогда и только тогда, когда выполняется для всех пар (a,b).

LaTeX

$$$\\forall {p : (\\Sigma' a, \\beta a) \\to \\mathrm{Prop}},\\ (\\\\forall x, p x) \\iff \\forall a b, p \\langle a,b \\rangle$$$

Lean4

theorem «forall» {p : (Σ' a, β a) → Prop} : (∀ x, p x) ↔ ∀ a b, p ⟨a, b⟩ :=
  ⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩

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