Stream: math-comp devs

Topic: rename disjoint_trans?

view this post on Zulip Christian Doczkal (Aug 19 2020 at 15:02):

Hi, I'm just having a look at the lemmas about disjoint and 

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 disjointWr and disjointW? Alternatively also disjointSl (subset left).

Last updated: Apr 19 2024 at 08:01 UTC