exists — Mathlib

English

A predicate p on ℂ has a witness x ∈ ℂ with p(x) if and only if there exist real a,b with p(a+bi).

Русский

Существует элемент z ∈ ℂ с p(z) тогда и только тогда, когда существуют действительное a,b с p(a+bi).

LaTeX

$$$$ (\exists z : \mathbb{C}, p(z)) \iff (\exists a,b \in \mathbb{R}, p(a + b i)). $$$$

Lean4

theorem «exists» {p : ℂ → Prop} : (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩ := by aesop

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