From 5e313e98d0f75d31d5b9da50112449ff74cec455 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 22 Apr 2024 08:36:56 +0200 Subject: [PATCH] doc: Classical.choice (#3871) Co-authored-by: Mario Carneiro --- src/Init/Classical.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 0d52a62e2e..1c6edb7978 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -15,6 +15,13 @@ namespace Classical noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} := choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩ +/-- +Given that there exists an element satisfying `p`, returns one such element. + +This is a straightforward consequence of, and equivalent to, `Classical.choice`. + +See also `choose_spec`, which asserts that the returned value has property `p`. +-/ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α := (indefiniteDescription p h).val