exists' — Mathlib

English

There is an equivalence between ∃ a,b, p a b and ∃ x : Σ a, β a, p x.1 x.2.

Русский

Между существованием ∃ a,b, p a b и ∃ x : Σ a, β a, p x.1 x.2 существует эквивалентность.

LaTeX

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

Lean4

theorem exists' {p : ∀ a, β a → Prop} : (∃ a b, p a b) ↔ ∃ x : Σ a, β a, p x.1 x.2 :=
  (Sigma.exists (p := fun x ↦ p x.1 x.2)).symm

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