Commit 2025-11-12 11:33 ae4938dd

View on Github →

feat: add contMDiffOn_empty and friends (#31542) On the empty set, the statement is vacuously true: this lemma is used in #30083 to eliminate some superfluous non-emptiness hypotheses.

Estimated changes