[Merged by Bors] - feat(analysis/normed_space): normed_group punit #7616
Conversation
semorrison
added
the
awaiting-review
| eq_of_dist_eq_zero := λ _ _ _, subsingleton.elim _ _, | ||
| dist_triangle := λ _ _ _, show (0:ℝ) ≤ 0 + 0, by rw add_zero, } | ||
|
|
||
| instance : metric_space punit := |
There was a problem hiding this comment.
Should we have the same for pempty and unit? It's really a shame that there isn't more defeq here...
There was a problem hiding this comment.
unit is an abbreviation for punit, so this instance should also work for unit (this is unfortunately not the case for empty/pempty)
There was a problem hiding this comment.
An option for empty/pempty is to merge #7606 first and add an instance is_empty -> metric_space.
There was a problem hiding this comment.
I vote just punting on this.
fpvandoorn
added
awaiting-author
semorrison
added
awaiting-review
|
Did you forget to push the change Johan requested?
This means that you vote to kick this into the queue, right? Fine by me. bors d+ |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
fpvandoorn
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
Minor content from LTE. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Minor content from LTE.