Commit 2026-01-29 16:43 98811970

feat(Logic/IsEmpty): add theorems relating surjectivity and emptiness (#33475) In particular, this adds a lemma saying that with an empty domain, a function is surjective iff its range is empty, and various forms of this.