feat: three misc lemmas about Hausdorff distance#10303
feat: three misc lemmas about Hausdorff distance#10303
Conversation
From sphere-eversion, I'm just submitting these.
| open Metric in | ||
| theorem IsCompact.exists_thickening_image [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} | ||
| {K : Set α} {U : Set β} (hK : IsCompact K) | ||
| (ho : IsOpen U) (hf : Continuous f) (hKU : MapsTo f K U) : |
There was a problem hiding this comment.
The assumption hf seems too strong here: isn't it enough to assume that f is continuous on K?
There was a problem hiding this comment.
It would seem so, but I don't think this actually holds. You need at least continuity in a neighbourhood containing K.
I presume continuity on a neighbourhood of K suffices. (I have proven an analogue of tendsto_nhdsSet with this assumption.) I can try to finish this lemma.
There was a problem hiding this comment.
I pushed the helper lemma: I'm not sure where the best place for it is.
NhdsSet is not possible (that file cannot import ContinuousOn; #find_home says ContinuousOn (which doesn't have other lemmas about NhdsSet yet). I put my new lemma at the end, and moved two related lemmas with it - and am not sure if this is the best call.
There was a problem hiding this comment.
I think that continuity at every point of K should be sufficient, no?
There was a problem hiding this comment.
(That's equivalent to ContinuousOn f K.)
Are you sure? The current proof in ContinuousOn.tendsto_nhdsSet requires more than that; I'm skeptical that this can be weakened.
There was a problem hiding this comment.
(I have finished proving generalising the "main lemma", requiring only continuity in a neighbourhood of K.)
There was a problem hiding this comment.
No, that's not equivalent to ContinuousOn f K, which only requires continuity within K while I'm requiring full continuity at those points.
Here is a sketch: at every point x of K, the map is continuous, so a small neighborhood is mapped to a small neighborhood, and in particular one can find a neighborhood of x whose image has a thickening contained in U, say by \epsilon_x. Then cover K by finitely many of such sets, call V their union, and let epsilon be the minimum of epsilon_x over these finitely many x. (I'd probably do the Lean proof using IsCompact.induction_on).
There was a problem hiding this comment.
💡 I will try implementing this, not before next weekend.
There was a problem hiding this comment.
I have now addressed this, and opened a new PR for simplicity: #20585.
Would you like to take a look again?
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
I will get to this PR eventually, but have other higher-priority things to do right now. If you're reading this, help jumping in and fixing the above is welcome. |
|
An updated version is available at #20585; let me close this PR in favour of that one. |
From sphere-eversion, I'm just submitting these.