exists — Mathlib

English

There is a symmetric version of exists: (∃ a, p a) ↔ ∃ a, p (ofMul a).

Русский

Существует симметричная версия существования: (∃ a, p a) ↔ ∃ a, p (ofMul a).

LaTeX

$$$\exists p:\ Additive α \to \mathrm{Prop},\ \exists a:\ Additive α,\ p(a) \iff \exists a:\ Additive α,\ p(\text{ofMul } a)$$$

Lean4

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

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