exists — Mathlib

English

For any predicate p on ULift α, there exists an element of ULift α satisfying p exactly when there exists an a in α such that p(up a).

Русский

Для произвольного предиката p на ULift α существование x с p x эквивалентно существованию a ∈ α такого, что p(up a).

LaTeX

$$$\\big(\\exists x : ULift\\,\\alpha,\\, p\,x\\big) \\iff \\big(\\exists a : \\alpha,\\, p(\\mathrm{up}(a))\\big)$$$

Lean4

@[simp]
theorem «exists» {p : ULift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (ULift.up x) :=
  up_surjective.exists

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