exists' — Mathlib

English

The existential quantifier over a product is equivalent to an existential 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

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

Lean4

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

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