doc: Classical.choice #3871
doc: Classical.choice #3871
Conversation
github-actions
bot
added
the
toolchain-available
| @@ -15,6 +15,11 @@ 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. | |||
There was a problem hiding this comment.
I stumbled a bit over "returns" here, which sounds very much like computation to me! I don't have a suggestion for a better word off the top of my head, though.
There was a problem hiding this comment.
is logically equivalent to an arbitrary such element
There was a problem hiding this comment.
I like the last two suggestions a lot here
There was a problem hiding this comment.
What about:
| Given that there exists an element satisfying `p`, returns one such element. | |
| Given that there exists an element of `α` that satisfies `p`, the result of `choose` is logically equivalent to an | |
| arbitrary such element. |
This makes the non-computational nature of it very apparent. We're also out in ultra-nitpick land here :)
There was a problem hiding this comment.
I'm not sure "the result of choose is logically equivalent to an arbitrary such element" is a well formed thing to say. I think I know the theorem it's alluding to but this is a really misleading way to say it. I think you might want to get some mathematician eyes on this
There was a problem hiding this comment.
Better to have the slight odor of computation than to write something that's incorrect :) I think that the discussion on this has now exceeded the very minor downsides of the word "returns", and am supportive of a merge as-is
There was a problem hiding this comment.
Using "logically equivalent" that way is sketchy and doesn't quite make sense for the technical meaning of logical equivalence. I like: "Given that there exists an element of α satisfying p, choose p denotes an otherwise arbitrary such element."
Co-authored-by: Mario Carneiro <[email protected]>
|
Mathlib CI status (docs):
|
|
Let's stick a fork in this one and call it done. |
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
No description provided.