exists — Mathlib

English

For any predicate p on WithBot α, existence of x with p x is equivalent to bottom or some a with p (a).

Русский

Для любого предиката p на WithBot α существование x с p x эквивалентно p(ниже) или существованию некоторого a с p(а).

LaTeX

$$$\\forall {p:WithBot α \\to Prop}, (\\exists x, p x) \\iff p(\\bot) \\lor \\exists a:α, p(\\mathrm{some}\\ a)$$$

Lean4

protected theorem «exists» {p : WithBot α → Prop} : (∃ x, p x) ↔ p ⊥ ∨ ∃ x : α, p x :=
  Option.exists

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