exists — Mathlib

English

For p : WithZero α → Prop, there exists x with p x if and only if p 0 or there exists a ∈ α with p (WithZero.coe a).

Русский

Для p: WithZero α → Prop существует x, такое что p x, тогда либо p 0, либо существует a ∈ α с p (WithZero.coe a).

LaTeX

$$$\exists x : WithZero \alpha, p\ x) \iff p(0) \lor \exists a : α, p(\mathrm{WithZero.coe}\ a)$$$

Lean4

@[to_additive]
theorem «exists» {p : WithZero α → Prop} : (∃ x, p x) ↔ p 0 ∨ ∃ a : α, p a :=
  Option.exists

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