Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-18 10:49 8f654ad4

View on Github →

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

Estimated changes

added theorem Prop.codisjoint_iff
added theorem Prop.disjoint_iff
added theorem Prop.is_compl_iff
modified theorem is_compl_iff
added theorem pi.codisjoint_iff
added theorem pi.disjoint_iff
added theorem pi.is_compl_iff