[Merged by Bors] - feat: three lemmas related to Hausdorff distance by grunweg · Pull Request #20585 · leanprover-community/mathlib4

grunweg · 2025-01-08T20:33:43Z

From sphere-eversion, I'm just submitting these.

Updated version of #10303.

github-actions · 2025-01-08T20:34:56Z

PR summary c2b75e87cb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ContinuousOn.tendsto_nhdsSet
+ IsCompact.exists_thickening_image_subset
+ infDist_pos_iff_not_mem_closure
+ thickening_ball

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.02)

Current number	Change	Type
59	1	large files

Current commit c2b75e87cb
Reference commit 8421da8699

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2025-01-09T20:32:15Z

Mathlib/Topology/MetricSpace/Thickening.lean

 /-- The (open) thickening `Metric.thickening δ E` of a fixed subset `E` is an increasing function of
 the thickening radius `δ`. -/
+@[gcongr]
 theorem thickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : Set α) :


This design decision may merit further discussion, as thickening is monotone in both delta and the E. I'm not sure which lemma is more useful...

Ruben-VandeVelde

Thanks! Some nits below

Mathlib/Topology/ContinuousOn.lean

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Mathlib/Topology/MetricSpace/Thickening.lean

grunweg · 2025-01-10T10:28:19Z

Thanks for the review nits; I have addressed them.

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Ruben-VandeVelde · 2025-01-10T20:37:18Z

maintainer merge

github-actions · 2025-01-10T20:37:38Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

PatrickMassot · 2025-01-10T22:51:56Z

bors merge

From sphere-eversion, I'm just submitting these. Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

mathlib-bors · 2025-01-10T23:15:43Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...

First two lemmas.

2b21269

grunweg added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jan 8, 2025

grunweg added 6 commits January 8, 2025 21:35

third lemma, TODO address comment

51fea44

wip: adapting proof

8bbc4bb

Enough for today

2805e3c

Remove superfluous assumption.

08cfb71

Almost done: one detail doesn't work out yet

afadefd

Solve that detail

9237564

grunweg changed the title ~~feat: two lemmas related to Hausdorff distance~~ feat: three lemmas related to Hausdorff distance Jan 9, 2025

grunweg mentioned this pull request Jan 9, 2025

feat: three misc lemmas about Hausdorff distance #10303

Closed

grunweg commented Jan 9, 2025

View reviewed changes

Superfluous assumption.

9585995

Ruben-VandeVelde reviewed Jan 10, 2025

View reviewed changes

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2025

Fix review nits

e399921

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2025

jcommelin requested a review from Ruben-VandeVelde January 10, 2025 19:35

Does this compile?

6086647

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Ruben-VandeVelde approved these changes Jan 10, 2025

View reviewed changes

Mathlib/Topology/MetricSpace/HausdorffDistance.lean Outdated Show resolved Hide resolved

Update Mathlib/Topology/MetricSpace/HausdorffDistance.lean

c2b75e8

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 10, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 10, 2025

mathlib-bors bot changed the title ~~feat: three lemmas related to Hausdorff distance~~ [Merged by Bors] - feat: three lemmas related to Hausdorff distance Jan 10, 2025

mathlib-bors bot closed this Jan 10, 2025

mathlib-bors bot deleted the MR-sphere-eversion-Hausdorff-distance2-v2 branch January 10, 2025 23:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: three lemmas related to Hausdorff distance#20585

[Merged by Bors] - feat: three lemmas related to Hausdorff distance#20585
grunweg wants to merge 11 commits intomasterfrom
MR-sphere-eversion-Hausdorff-distance2-v2

grunweg commented Jan 8, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 8, 2025 •

edited

Loading

Declarations diff

Uh oh!

grunweg Jan 9, 2025

Uh oh!

Ruben-VandeVelde left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jan 10, 2025

Uh oh!

Uh oh!

Ruben-VandeVelde commented Jan 10, 2025

Uh oh!

github-actions bot commented Jan 10, 2025

Uh oh!

PatrickMassot commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

grunweg commented Jan 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c2b75e87cb

Import changes for modified files

Declarations diff

Uh oh!

grunweg Jan 9, 2025

Choose a reason for hiding this comment

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jan 10, 2025

Uh oh!

Uh oh!

Ruben-VandeVelde commented Jan 10, 2025

Uh oh!

github-actions bot commented Jan 10, 2025

Uh oh!

PatrickMassot commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

grunweg commented Jan 8, 2025 •

edited

Loading

github-actions bot commented Jan 8, 2025 •

edited

Loading