forall — Mathlib

English

A specialized equivalent form: (forall x, p x) is equivalent to forall a,b, p ⟨a,b⟩.

Русский

Эквивалентная форма: (для всех x, p x) эквивалентно forall a,b, p ⟨a,b⟩.

LaTeX

$$$ \forall {x : (\alpha \times \beta)}, 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⟩

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