exists — Mathlib

English

There exists an x with p x if and only if there exist a,b with p ⟨a,b⟩.

Русский

Существует x such that p x тогда и только тогда, когда существуют a,b с p ⟨a,b⟩.

LaTeX

$$$\\exists x, p x \\iff \\exists a\\, b, p \\langle a,b\\rangle$$$

Lean4

@[simp]
theorem «exists» {p : (Σ' a, β a) → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ :=
  ⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

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