exists — Mathlib

English

For any predicate p on Colex α, there exists an a with p a iff there exists an a with p (toColex a).

Русский

Для любого свойства p на Colex α существует элемент, удовлетворяющий p, эквивалентно существованию элемента, удовлетворяющего p(toColex a).

LaTeX

$$$\\forall p:\\\\ Colex\\,α \\to \\text{Prop},\\; (\\exists a:\\\\ Colex\\,α,\\\\ p(a)) \\iff (\\exists a:\\\\ α,\\\\ p(toColex\\,a))$$$

Lean4

@[simp]
theorem «exists» {p : Colex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toColex a) :=
  Iff.rfl

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