Zulip Chat Archive

Stream: new members

Topic: Showing X is a subset of itself


view this post on Zulip Anna Hollands (Jun 29 2020 at 23:10):

Hi! I'm trying to prove a lemma that requires me to find a subset of a set X st.... X works, but use X doesn't. How do I get it to recognise X as a valid subset of X?

view this post on Zulip Patrick Massot (Jun 29 2020 at 23:11):

(univ : set X) is what you are looking for.

view this post on Zulip Patrick Massot (Jun 29 2020 at 23:12):

X has type Type u for some universe u. It doesn't have type set X.


Last updated: May 08 2021 at 04:14 UTC