Stream: math-comp users

Topic: Goal involving set intersection


view this post on Zulip Julin Shaji (Mar 21 2024 at 06:35):

Given a goal like:

Goal
  ([set tt] :&: [set tt] != set0).
Proof.

How can one show this to be correct?

Couldn't figure out how to properly get rid of :&:.

view this post on Zulip Julin Shaji (Mar 21 2024 at 06:59):

Okay got rid of :&: with setIid. Now stuck on [set tt] != set0..

view this post on Zulip Quentin VERMANDE (Mar 21 2024 at 08:08):

You can turn this into ~ [set tt] == set0 with negP, or into ~ [set tt] = set0 with eqP.

view this post on Zulip Cyril Cohen (Mar 21 2024 at 09:06):

I guess this might be the most efficient way to conclude:
https://github.com/math-comp/math-comp/blob/14411700e3fad6297ccb682ad5a7955ff8202b08/mathcomp/ssreflect/finset.v#L736C1-L737C51


Last updated: Jul 25 2024 at 16:02 UTC