Commit 2026-03-27 16:34 251d9c0f

View on Github →

chore: new file for sets closed under directed suprema (#37273) I plan to add more material to this file in the near future, and I figured it might be good to give it its own place.

Estimated changes

deleted theorem DirSupClosed.inter
deleted def DirSupClosed
deleted theorem DirSupInacc.dirSupInaccOn
deleted theorem DirSupInacc.union
deleted def DirSupInacc
deleted theorem DirSupInaccOn.mono
deleted def DirSupInaccOn
deleted theorem IsLowerSet.dirSupInacc
deleted theorem IsUpperSet.dirSupClosed
deleted theorem dirSupClosed_Iic
deleted theorem dirSupClosed_compl
deleted theorem dirSupInaccOn_univ
deleted theorem dirSupInacc_compl