Stream: math-comp users

Topic: ✔ how ot use =i? in example undup s i= s


view this post on Zulip Andrey Klaus (Nov 12 2021 at 13:31):

Hello.
I have x \in undup s, I would like to prove x \in s. What I found about it is that undup s i= s. How to prove that x \in s ?

view this post on Zulip Andrey Klaus (Nov 12 2021 at 13:35):

I mean is there a way to use undup s i= s for this proof or should I use the induction? If there is such way, it would be greate to have an example.

view this post on Zulip Laurent Théry (Nov 12 2021 at 13:37):

If you have H : undup s =i s, you can use it to rewrite, try to see what =i means by setting have H1 := H x.

view this post on Zulip Andrey Klaus (Nov 12 2021 at 14:38):

Great thank you! It is what I need.

view this post on Zulip Notification Bot (Nov 13 2021 at 23:18):

Andrey Klaus has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC