[Merged by Bors] - feat: behavior of Cauchy under operations on UniformSpace
#6694
Conversation
ADedecker
added
awaiting-review
t-topology
| lemma cauchy_iInf_uniformSpace' {ι : Sort*} {u : ι → UniformSpace β} | ||
| {l : Filter β} [l.NeBot] : | ||
| Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l := by | ||
| simp_rw [cauchy_of_neBot (uniformSpace := _), iInf_uniformity, le_iInf_iff] |
There was a problem hiding this comment.
What is this (uniformSpace := _) dark magic? Is it acting on elaboration order?
There was a problem hiding this comment.
Without it Lean tries to guess the uniform structure by typeclass inference, so it doesn't work.
There was a problem hiding this comment.
| have := fun i ↦ (hl i).1 | ||
| simpa [cauchy_pi_iff] | ||
|
|
||
| instance Pi.complete [∀ i, CompleteSpace (α i)] : CompleteSpace (∀ i, α i) where |
There was a problem hiding this comment.
I'm still a bit sad that we don't prove this by abstract non-sense after constructing the completion functor, but I can live with that.
| @@ -20,7 +20,7 @@ open Filter TopologicalSpace Set Classical UniformSpace Function | |||
|
|
|||
| open Classical Uniformity Topology Filter | |||
|
|
|||
| variable {α : Type u} {β : Type v} [UniformSpace α] | |||
| variable {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] | |||
There was a problem hiding this comment.
Why did you add this name?
There was a problem hiding this comment.
To allow for Cauchy (uniformSpace := u) instead of @Cauchy _ u, as well as the (uniformSpace := _) dark magic (instead of @s and _s). I'm not sure the benefit is very clear, but I think it is more readable.
There was a problem hiding this comment.
Oh I see. Maybe we should have a general strategy about this, but in this case it clearly helps since I was able to understand the proofs without realizing this trick was needed..
|
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Some of the lemmas are cherry-picked from leanprover-community/mathlib#17975 and will be useful for the general Arzela-Ascoli theorem, but I also filled some API holes on the way.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Cauchy under operations on UniformSpaceCauchy under operations on UniformSpace
Some of the lemmas are cherry-picked from leanprover-community/mathlib#17975 and will be useful for the general Arzela-Ascoli theorem, but I also filled some API holes on the way.