Zulip Chat Archive

Stream: general

Topic: inter_subset_union


view this post on Zulip Johan Commelin (Feb 05 2020 at 19:25):

Am I stupid, or are we missing s \cap t \sub s \cup t in the library?

view this post on Zulip Kevin Buzzard (Feb 05 2020 at 19:31):

I know two proofs of that, maybe they couldn't decide which one to use

view this post on Zulip Kevin Buzzard (Feb 05 2020 at 19:31):

Do we have P and Q implies P or Q?

view this post on Zulip Jesse Michael Han (Feb 05 2020 at 19:53):

due to some auspicious [ematch] lemmas in the lattice library, the version for lattices is by {[smt] eblast}

but indeed, library_search fails for the lattice version also.

view this post on Zulip Yury G. Kudryashov (Feb 05 2020 at 20:05):

BTW, where can I read about ematch?


Last updated: May 08 2021 at 18:17 UTC