mathlib3
feat(topology/uniform_space/uniform_convergence_topology): prove completeness
#18017
Open

feat(topology/uniform_space/uniform_convergence_topology): prove completeness #18017

ADedecker wants to merge 13 commits into master from AD_uniform_convergence_complete
ADedecker
ADedecker Begin
713045bd
ADedecker Initial commit
4cdb798b
ADedecker First part done
ff0d0dd2
ADedecker Initial commit
1fce757a
ADedecker More progress
0c945817
ADedecker Done?
e791b928
ADedecker Done?
ad6bbd2f
ADedecker Fix
e80bbbe4
ADedecker Main lemma done
5b2313e3
ADedecker Need merge
652e38a0
ADedecker Merge branch 'AD_uniform_convergence_generated_bornology' into AD_uni…
fad5afdd
ADedecker Done!
e56649fb
ADedecker ADedecker added WIP
ADedecker Shorten proofs
090c3f0a
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
Milestone