exists — Mathlib

English

For any predicate p on α^{op}, (∃ a, p(a)) is equivalent to ∃ a: α, p(op a).

Русский

Для любого предиката p на α^{op} имеем эквивалентность: (существует a, p(a)) эквивалентно ∃ a∈α, p(op(a)).

LaTeX

$$$\\\\exists a:\\\\alpha, \\\\; p(a) \\\\iff \\\\exists a:\\\\alpha, \\\\; p(\\\\mathrm{op}(a))$$$

Lean4

@[to_additive (attr := simp)]
theorem «exists» {p : αᵐᵒᵖ → Prop} : (∃ a, p a) ↔ ∃ a, p (op a) :=
  op_surjective.exists

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