Is there an existing lemma in `finset`

or `fintype`

that can extract `(x: T) (px: P x)`

from `#|[set x | P x]| >0`

or `exists x, P x`

? In general I've understood that you can't because of something technical about "case analysis on Type", but when `T`

is `finType`

everything should be possible. I've proven this in my project, but I think that something this simple and useful should be a lemma in the library.

maybe look in choice.v / countable, I don't think you need finitude for that

Thanks, `sigW: forall [T : choiceType] [P : pred T], (exists x : T, P x) -> {x : T | P x}`

is in `choice.v`

.

Enrico Tassi has marked this topic as resolved.

This is also known as an "existential witness operator" or "constructive indefinite description" (when used as an axiom).

Last updated: Jul 23 2024 at 21:01 UTC