Stream: math-comp analysis

Topic: Proof by contradiction with set0


view this post on Zulip Julien Puydt (Oct 17 2022 at 10:12):

I managed to have both H1: V1 & V2 == set0 and H2: V1 & V2 != set0 in my context (with back-quoted, it's a setI), with goal False (exfalso tends to do that), but I don't get how to finish the proof. I thought I could get away with exact H2 H2, but I get issues with is_true...

view this post on Zulip Cyril Cohen (Oct 17 2022 at 10:38):

Either of these should do the trick:

view this post on Zulip Cyril Cohen (Oct 17 2022 at 10:39):

BTW, if you want to insert backquotes inside backquoted markdown you only need to add a backquote to the outermost ones, as in ``H1 : V1 `&` V2 == set0``


Last updated: Jan 30 2023 at 11:03 UTC