Commit 2025-11-28 16:39 5f80bf59

View on Github →

feat: grind annotations for Disjoint (#28026)

Estimated changes

modified theorem Set.disjoint_iff_forall_ne
modified theorem Set.not_disjoint_iff
modified theorem Codisjoint.eq_iff
modified theorem Codisjoint.ne_iff
added theorem Codisjoint.out
modified theorem Disjoint.eq_iff
modified theorem Disjoint.ne_iff
added theorem Disjoint.out
modified theorem codisjoint_assoc
modified theorem codisjoint_left_comm
modified theorem codisjoint_right_comm