choose — Mathlib

English

From a nontrivial set, one can extract two distinct elements a and b with a ∈ s, b ∈ s, and a ≠ b (noncomputable choice).

Русский

Из подсинглотного множества можно выбрать два различных элемента a и b, принадлежащих этому множеству (пользуется аксиомой выбора).

LaTeX

$$$ \exists a\in s, \exists b\in s, a\neq b $$$

Lean4

/-- Extract witnesses from s.nontrivial. This function might be used instead of case analysis on the
argument. Note that it makes a proof depend on the classical.choice axiom. -/
protected noncomputable def choose (hs : s.Nontrivial) : α × α :=
  (Exists.choose hs, hs.choose_spec.right.choose)

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