Zulip Chat Archive

Stream: general

Topic: inter_subset_union

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?

Kevin Buzzard (Feb 05 2020 at 19:31):

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

Kevin Buzzard (Feb 05 2020 at 19:31):

Do we have P and Q implies P or Q?

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.

Yury G. Kudryashov (Feb 05 2020 at 20:05):

BTW, where can I read about ematch?

Last updated: Aug 03 2023 at 10:10 UTC