Commit 2026-04-03 20:24 5fbb6779

View on Github →

feat: DirSupClosedOn (#37616) This is to DirSupClosed as DirSupInaccOn is to DirSupInacc. We also add some basic API.

Estimated changes

added theorem DirSupClosedOn.mono
added def DirSupClosedOn
modified theorem DirSupInacc.dirSupInaccOn
modified theorem DirSupInaccOn.mono
added theorem dirSupClosedOn_compl
added theorem dirSupClosedOn_univ
modified theorem dirSupClosed_compl
added theorem dirSupInaccOn_compl
modified theorem dirSupInacc_compl