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: Oct 13 2024 at 01:02 UTC