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.

view this post on Zulip Notification Bot (Aug 06 2022 at 09:27):

Enrico Tassi has marked this topic as resolved.

view this post on Zulip Alexander Gryzlov (Aug 08 2022 at 23:15):

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


Last updated: Mar 28 2024 at 11:01 UTC