exists — Mathlib

English

The rational exists lemma relates the standard existential quantifier over rationals to an existential over integers: ∃ r, p r is equivalent to ∃ a,b ∈ ℤ, b ≠ 0 ∧ p(a/b).

Русский

Лемма существования рационального числа связывает существование по рационалям с существованием по парам целых чисел.

LaTeX

$$$\\exists r\\, p(r) \\iff \\exists a,b \\in \\mathbb{Z},\\ b \\neq 0 \\land p\\left(\\frac{a}{b}\\right)$$$

Lean4

protected theorem «exists» {p : ℚ → Prop} : (∃ r, p r) ↔ ∃ a b : ℤ, b ≠ 0 ∧ p (a / b) := by
  simpa using Rat.forall (p := (¬p ·)).not

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