exists_iff — Mathlib

English

Let p be a predicate on DegLex α. Then there exists x in DegLex α with p(x) iff there exists a in α with p(toDegLex(a)).

Русский

Пусть p — предикат на DegLex α. Существуют x ∈ DegLex α такие, что p(x) выполняется, если и только если существует a ∈ α такое, что p(toDegLex(a)).

LaTeX

$$$(\exists x:\DegLex(\alpha),\ p(x)) \iff \exists a:\alpha,\ p(toDegLex(a))$$$

Lean4

@[simp]
theorem exists_iff {p : DegLex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toDegLex a) :=
  Iff.rfl

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