exists — Mathlib

English

Let p be a predicate on NNReal. Then there exists an x in NNReal with p(x) if and only if there exists x in ℝ with hx ≥ 0 and p(⟨x, hx⟩).

Русский

Пусть p — предикат на NNReal. Тогда существует x ∈ NNReal с p(x) тогда и только тогда, когда существует x ∈ ℝ с hx ≥ 0 и p(⟨x, hx⟩).

LaTeX

$$$ (\exists x : \mathbb{R}_{\ge 0}, p x) \iff \exists x : \mathbb{R}, \exists hx : 0 \le x, p \langle x, hx \rangle \,$$$

Lean4

protected theorem «exists» {p : ℝ≥0 → Prop} : (∃ x : ℝ≥0, p x) ↔ ∃ (x : ℝ) (hx : 0 ≤ x), p ⟨x, hx⟩ :=
  Subtype.exists

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