Commit 2026-06-08 10:43 67f29516
View on Github →feat: CountableSupClosed (#38245)
Define the property for a set of being closed by countable supremum (resp. infimum).
The new file is adapted from the SupClosed file, which describes sets closed by binary supremum.
CountableInfClosed will be used in measure theory, for developments related to compact systems used for Kolmogorov's extension theorem and Choquet's capacitability theorem.