exists — Mathlib

English

There exists an element with property p on PLift α if and only if there exists an a in α with p(up a).

Русский

Существует элемент с свойством p на PLift α тогда и только тогда, когда существует a в α such, что p(up(a)).

LaTeX

$$$\\forall {p : \\mathrm{PLift} \\alpha \\rightarrow \\mathrm{Prop}}, \\bigl(\\exists x \\in \\mathrm{PLift} \\alpha, p(x)\\bigr) \\Leftrightarrow \\bigl(\\exists x : \\alpha, p(\\mathrm{up}(x))\\bigr)$$$

Lean4

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

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