Hi, I'm just having a look at the lemmas about
Lemma disjoint_trans A B C : A \subset B -> [disjoint B & C] -> [disjoint A & C].
seems like an odd/poor choice. How about deprecating this name in favor of something like
disjointWl (weaken left) and adding
disjointW? Alternatively also
disjointSl (subset left).
Last updated: Feb 09 2023 at 03:06 UTC