bex_def — Mathlib

English

For predicates p and q on α, there is an equivalence between (∃ x : α, ∃ h : p x, q x) and ∃ x : α, p x ∧ q x.

Русский

Для предикатов p и q на α существует эквивалентность между (∃ x : α, ∃ h : p x, q x) и ∃ x : α, p x ∧ q x.

LaTeX

$$$\exists x:\, \exists h: p(x), q(x) \quad\iff\quad \exists x:\, p(x) \land q(x)$$$

Lean4

theorem bex_def : (∃ (x : _) (_ : p x), q x) ↔ ∃ x, p x ∧ q x :=
  ⟨fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩, fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩⟩

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