metric namespace #568
metric namespace #568
Conversation
|
See https://github.com/leanprover-community/mathlib/tree/metric_namespace as an alternative way (there is a short Zulip discussion) |
|
I have added Mario's proposition to the PR. It looks like a reasonable middle ground, putting in dedicated namespaces the notions that could conflict with notions in other fields, but keeping in the root namespace notions that are directly defined in terms of |
sgouezel
force-pushed
the
metric_namespace
branch
from
c52f094
to
86d771b
Compare
analysis/normed_space.lean
Outdated
| @@ -340,11 +340,14 @@ begin | |||
| have limg' : tendsto (λ x, ∥g x∥) e (nhds ∥b∥) := filter.tendsto.comp limg (continuous_iff_tendsto.1 continuous_norm _), | |||
|
|
|||
| have lim1 : tendsto (λ x, ∥f x - s∥ * ∥g x∥) e (nhds 0), | |||
| by simpa using tendsto_mul limf' limg', | |||
| { have := tendsto_mul limf' limg', | |||
There was a problem hiding this comment.
uh, this is not good. Why is this necessary?
There was a problem hiding this comment.
There was a problem hiding this comment.
Changed to a better version suggested by P. Massot.
There was a problem hiding this comment.
Thanks @rwbarton for the reference. I hope with the simpa-change we can remove these changes here.
There was a problem hiding this comment.
Definitely. I confirm that with the simpa version proposed by @rwbarton, the change is not needed any more.
There was a problem hiding this comment.
okay, I will merge @rwbarton s simpa-change and then this PR
There was a problem hiding this comment.
I just opened a PR with the changes to simpa (including doc changes).
There was a problem hiding this comment.
Too late, I already pushed :-)
analysis/normed_space.lean
Outdated
| have limg3 := tendsto_iff_norm_tendsto_zero.1 limg, | ||
| have lim2 : tendsto (λ x, ∥s∥ * ∥g x - b∥) e (nhds 0), | ||
| by simpa using tendsto_mul tendsto_const_nhds limg3, | ||
|
|
||
| { have := tendsto_mul tendsto_const_nhds limg3, |
|
merged in 49c059a |
|
Thanks @sgouezel for this change! |
Currently, all the notions about metric spaces are in the root namespace, contrary to essentially everything else in mathlib. This PR adds a metric namespace, puts the notions related to metric spaces in it, and opens it where necessary.
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list