Zulip Chat Archive

Stream: new members

Topic: Subset of subset


Thomas Browning (Jul 29 2020 at 23:46):

If B : set C, and A : set B, how do you get (a version of) A in set C?

Adam Topaz (Jul 29 2020 at 23:51):

Try something like subtype.val '' A

Yury G. Kudryashov (Jul 30 2020 at 03:45):

We recently decided that the simp-normal form is coe, not subtype.val.

Yury G. Kudryashov (Jul 30 2020 at 03:45):

So, (coe '' A : set C)

Eric Wieser (Aug 08 2020 at 10:13):

By this, you mean that we should never type subtype.val or x.val in a proof or lemma?

Reid Barton (Aug 08 2020 at 11:41):

No, this is much too strong. Just don't use it in the statement of a simp lemma, especially on the left-hand side. You might find it useful to avoid using it in other places too.

Kevin Buzzard (Aug 10 2020 at 12:09):

@Eric Wieser do you know about simp normal form? The idea is that if you want to get simp working for you, you should know what the form is which the lemmas are trying to normalise towards. The idea is that when your goal is in the "right" form when you can just apply standard theorems, but all the theorems need to be stated in the "right" form too. So you need to make some design decision about what all your lemmas will look like, and then try and stick to this notation in the middle of proofs.


Last updated: Dec 20 2023 at 11:08 UTC