Commit 2025-07-11 02:59 f2ee88f6

View on Github →

feat: the composition of open relations is open (#24173) Zulip

Estimated changes

added theorem IsOpen.relComp