Stream: math-comp users

Topic: ✔ sigma type from exists


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: Feb 08 2023 at 07:02 UTC