basic facts for emetric spaces #608
Conversation
|
Interesting. There is a bit more structure of interest in emetric balls; in particular infinity balls are equivalence classes and every point is the center of one (i.e. they have the ultrametric property). Also there is a common construction that takes an emetric space and a point in the space (zero) and constructs a metric space out of the infinity ball around it. Things like L^p, l^p and even bcfs fall in this category. Usually it is in the normed group context, but that would require extending to enormed groups. |
|
I agree with all you say, especially on the construction of L^p. |
| variables {x y z : α} {ε ε₁ ε₂ : ennreal} {s : set α} | ||
|
|
||
| /-- `eball x ε` is the set of all points `y` with `dist y x < ε` -/ | ||
| def eball (x : α) (ε : ennreal) : set α := {y | edist y x < ε} |
There was a problem hiding this comment.
I think this can just be called ball; it's already namespaced.
Adds basic facts on emetric spaces that are already available on metric spaces. In particular, balls in emetric spaces (denoted
eball) and basic properties of neighborhoods or convergence.Some facts that were proved for metric spaces but hold for emetric spaces are transferred from the metric to the emetric spaces, notably first countability, or the fact that separable implies second countable, or the fact that a compact set admits a countable dense subset. The proofs are direct adaptations of the ones for metric spaces.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list