mathlib3
feat(topology/metric_space/path_metric): Definition of the path metric on a metric space and proof of its idempotency
#18375
Open
Open
feat(topology/metric_space/path_metric): Definition of the path metric on a metric space and proof of its idempotency #18375
bottine
wants to merge
41 commits into
master
from
bottine/topology.metric_space.path_metric_second_go
?
db6f61a2
go
81e237a3
continuous_on -> continuous for simplicity
37d90e77
?
fb3603f6
advances
01056d87
yes
d2914a42
continuity nocheckmark but no bad
f351fd27
cleaner?
6f9f77f3
cleaner
db0ff88a
.
2e86f3b1
dirty commit
3dcbd8d0
dirty, but not so dirty
a4158e7a
non-prime in terms of prime
73bdfc83
move stuff to evariation_on
056fdcdb
ok
ff83575e
ok
da07ceb9
misc
05a3c14b
mirc'
09123e59
misc
593fba3b
set.ord_connected and fewer sorries
39dce34e
@alreadydone's code
408e87fa
merge master
8a25bc3d
starting to reorganize towards PR?
15393f4c
yes
e4202efd
commit just to get the CI to build mathlib for me
c30b11aa
commit just to get the CI to build mathlib for me
66a1d36b
moving things where I think they belong
2533e44f
TODO'd lemma done
1b7a7df1
this and that
453b8c5b
yes
418d3d5b
yes
ad891001
bottine
commented
on 2023-02-03
so that #lint doesn't complain
59f2647a
trying to organize things
11f80bf4
trying to organize things
c7d92861
barh
9b0052b5
it typechecks
58d54abe
minor things
98de114d
minor things
587cf96c
bottine
changed the title 
lint
b7b02cfa
Junyan's suggestions
bfbb7480
typo
29452afe
bottine
commented
on 2023-02-20
urkud
commented
on 2023-06-21
Reviewers
Assignees
No one assigned
Labels
awaiting-author
t-topology
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub