exists' — Mathlib

English

A wrapper stating that there exists over PProd is equivalent to exists over both coordinates a and b.

Русский

Обобщение exists над PProd эквивалентно существованию по координатам a и b.

LaTeX

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

Lean4

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

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