[Merged by Bors] - feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets #10188
Conversation
…mmas about open thickenings of subsets
kkytola
added
the
awaiting-review
sgouezel
added
awaiting-author
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
I added a file-level docstring about the definition of |
|
I don't understand the failed check (CI / build mathlib (push)), this compiles on my computer. |
kkytola
added
awaiting-review
|
I have restarted the build |
Thank you! I still don't understand the new failure; now "CI / build mathlib (push)" works but "CI / run tests (push)" fails. |
|
✌️ kkytola can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…ty/mathlib into kkytola/thickenings_1
|
bors r+ |
…mmas about open thickenings of subsets (#10188) Add definition and basic API about open thickenings of subsets in metric spaces, in preparation for the portmanteau theorem on characterizations of weak convergence of Borel probability measures. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Add definition and basic API about open thickenings of subsets in metric spaces, in preparation for the portmanteau theorem on characterizations of weak convergence of Borel probability measures.
This is a (rather independent) part of my attempt to PR a proof of the portmanteau theorem https://github.com/kkytola/lean_portmanteau. Specifically it is intended as an improved and cleaned up version of a manageable size chunck of the file https://github.com/kkytola/lean_portmanteau/blob/main/portmanteau_metric_lemmas.lean.
If this PR's style is the right way to do thickenings, then I will follow up by closed thickenings, intersections of thickenings in relation to closures, continuous approximations of indicator functions of closed sets, and crucially, the countability of thickening-radii such that the boundary of the thickening carries a positive measure w.r.t. a given Borel probability measure.