choose_spec — Mathlib

English

If there exists an element a in l with p a, then choose p l hp is an element of l and satisfies p.

Русский

Если существует элемент a в l, такой что p a, то choose p l hp является элементом l и удовлетворяет p.

LaTeX

$$$ \\exists a\\ a\\in l \\land p a \\Rightarrow (\\text{choose } p l hp) \\in l \\land p (\\text{choose } p l hp) $$$

Lean4

theorem choose_spec (hp : ∃ a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
  (chooseX p l hp).property

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