[Merged by Bors] - feat(analysis/normed_space/pointwise): Balls disjointness #13379
Conversation
YaelDillies
added
the
awaiting-review
|
|
||
| /-- In a real normed space, the image of the unit ball under scalar multiplication by a positive | ||
| constant `r` is the ball of radius `r`. -/ | ||
| lemma smul_unit_ball_of_pos {r : ℝ} (hr : 0 < r) : r • ball 0 1 = ball (0 : E) r := | ||
| by rw [smul_unit_ball hr.ne', real.norm_of_nonneg hr.le] | ||
|
|
||
| -- This is also true for `ℚ`-normed spaces |
There was a problem hiding this comment.
What exactly do you need in order to generalize this?
There was a problem hiding this comment.
Nothing. Everything is here (namely exists_rat_btwn). What I'm afraid of is that writing those lemmas as normed_space ℚ E won't make them directly applicable to normed_space ℝ E. Maybe I'm wrong?
There was a problem hiding this comment.
Okay, it's indeed not automatic, but could be made so if we were able to ensure everything is defeq for char zero division rings when adding the normed_space ℝ E → normed_space ℚ E instance (similar to normed_space.complex_to_real).
So what about we just leave it as is for now and worry about it when we will actually deal with ℚ-normed spaces?
There was a problem hiding this comment.
I was wondering whether ℝ could be replaced by a suitable normed field K. For some definition of "suitable".
There was a problem hiding this comment.
But I'm happy to leave it as it is for now.
There was a problem hiding this comment.
I think the answer is linear_ordered_nondiscrete_normed_field, which doesn't currently exist.
|
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
|
||
| /-- In a real normed space, the image of the unit ball under scalar multiplication by a positive | ||
| constant `r` is the ball of radius `r`. -/ | ||
| lemma smul_unit_ball_of_pos {r : ℝ} (hr : 0 < r) : r • ball 0 1 = ball (0 : E) r := | ||
| by rw [smul_unit_ball hr.ne', real.norm_of_nonneg hr.le] | ||
|
|
||
| -- This is also true for `ℚ`-normed spaces |
There was a problem hiding this comment.
But I'm happy to leave it as it is for now.
leanprover-community-bot-assistant
added
the
ready-to-merge
Two balls in a real normed space are disjoint iff the sum of their radii is less than the distance between their centers.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Two balls in a real normed space are disjoint iff the sum of their radii is less than the distance between their centers.
I could also add versions with a sphere and a ball, if you want me to.