Stream: math-comp users

Topic: sigma type from exists


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Aug 06 2022 at 07:51):

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

view this post on Zulip 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