feat(Topology/Compactness/CompactSystem): introduce compact Systems#25899
Closed
pfaffelh wants to merge 4477 commits intoleanprover-community:masterfrom
Closed
feat(Topology/Compactness/CompactSystem): introduce compact Systems#25899pfaffelh wants to merge 4477 commits intoleanprover-community:masterfrom
pfaffelh wants to merge 4477 commits intoleanprover-community:masterfrom
Conversation
Loading
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
20 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A compact system is a set systems with the property that, whenever a countable intersections of sets in the set system is empty, there is a finite subset of sets with empty intersection. These are needed e.g. in measure theory if one wants to show sigma-additivity of a set function on a ring.
univ, is a compact system.Dissipate s x := ⋂ y ≤ x, s y(Data/Set/Dissipate), which is parallel to Data/Set/Accumulate.Co-authored-by: Rémy Degenne remydegenne@gmail.com
This PR continues the work from #24541.
Original PR: #24541