[Merged by Bors] - feat(Order/Filter) : add 2 constructors #9200
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add two definitions to create filter from a property on sets: - Filter.ofProp_finite_inter if the property is stable under finite intersections and set enlargements. - Filter.ofProp_finite_union if the property is stable under finite unions and set shrinking. Filter.ofProp_finite_union is the key ingredient in IsCompact.induction_on but may be convenient to have as individual building block. Both results also specialise to properties that are stable under countable unions/intersections, in which case the filter is a CountableInterFilter. This plays a role in IsLindelof.induction_on and will be added when this PR is accepted.
JADekker
added
awaiting-review
urkud
reviewed
Dec 23, 2023
urkud
reviewed
Dec 23, 2023
urkud
added
awaiting-author
Rename Filter.ofProp_finite_union to Filter.comk Remove Filter.ofProp_finite_inter
JADekker
added
awaiting-review
|
I added |
urkud
added
awaiting-author
urkud
changed the title
JADekker
added
awaiting-review
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
|
This PR/issue depends on:
|
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by urkud. |
leanprover-community-mathlib4-bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 2, 2024
Add two constructors to create filters from a property on sets:
- `Filter.comk` if the property is stable under finite unions and set shrinking.
- `Filter.ofCountableUnion` if the property is stable under countable unions and set shrinking
`Filter.comk` is the key ingredient in `IsCompact.induction_on` but may be convenient to have as individual building block.
A `Filter` generated by `Filter.ofCountableUnion` is a `CountableInterFilter`, which is given by the instance `Filter.countableInter_ofCountableUnion`.
### Other changes
- Use `Filter.comk` for `Filter.cofinite`, `Bornology.ofBounded` and `MeasureTheory.Measure.cofinite`.
- Use `Filter.ofCountableUnion` for `MeasureTheory.Measure.ae`.
- Use `{_ : Bornology _}` instead of `[Bornology _]` in some lemmas so that `rw/simp` work with non-instance bornologies.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Build failed: |
|
Does the failure of the build relate to the cache issues recently discussed on Zulip? |
Topology/Compactness/Compact now imports Order/Filter/Basic to have access to Filter.comk
|
I've fixed the import issue, now everything seems to work! |
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 4, 2024
Add two constructors to create filters from a property on sets:
- `Filter.comk` if the property is stable under finite unions and set shrinking.
- `Filter.ofCountableUnion` if the property is stable under countable unions and set shrinking
`Filter.comk` is the key ingredient in `IsCompact.induction_on` but may be convenient to have as individual building block.
A `Filter` generated by `Filter.ofCountableUnion` is a `CountableInterFilter`, which is given by the instance `Filter.countableInter_ofCountableUnion`.
### Other changes
- Use `Filter.comk` for `Filter.cofinite`, `Bornology.ofBounded` and `MeasureTheory.Measure.cofinite`.
- Use `Filter.ofCountableUnion` for `MeasureTheory.Measure.ae`.
- Use `{_ : Bornology _}` instead of `[Bornology _]` in some lemmas so that `rw/simp` work with non-instance bornologies.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Add two constructors to create filters from a property on sets:
Filter.comkif the property is stable under finite unions and set shrinking.Filter.ofCountableUnionif the property is stable under countable unions and set shrinkingFilter.comkis the key ingredient inIsCompact.induction_onbut may be convenient to have as individual building block.A
Filtergenerated byFilter.ofCountableUnionis aCountableInterFilter, which is given by the instanceFilter.countableInter_ofCountableUnion.Other changes
Filter.comkforFilter.cofinite,Bornology.ofBoundedandMeasureTheory.Measure.cofinite.Filter.ofCountableUnionforMeasureTheory.Measure.ae.{_ : Bornology _}instead of[Bornology _]in some lemmas so thatrw/simpwork with non-instance bornologies.