Alex Loiko (Aug 06 2022 at 07:12): Alex Loiko (Aug 06 2022 at 07:12):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.
Enrico Tassi (Aug 06 2022 at 07:51):maybe look in choice.v / countable, I don't think you need finitude for that
Alex Loiko (Aug 06 2022 at 08:16):Thanks, sigW: forall [T : choiceType] [P : pred T], (exists x : T, P x) -> {x : T | P x} is in choice.v.
Last updated: Jan 29 2023 at 19:02 UTC