inter_subset_union

Stream: general

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Do we have P and Q implies P or Q?

[Jesse Michael Han]

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]

BTW, where can I read about ematch?