mathlib3
8f654ad4 - chore(order/bounded_order): lemmas about disjoint on prod, pi, and Prop (#17500)

Commit

3 years ago

chore(order/bounded_order): lemmas about disjoint on prod, pi, and Prop (#17500) Also adds `codisjoint` and `is_compl` lemmas.

Author

eric-wieser

Parents