mathlib3
feat(topology/uniform_space/ascoli): general Arzela-Ascoli theorem
#17975
Open

feat(topology/uniform_space/ascoli): general Arzela-Ascoli theorem #17975

ADedecker wants to merge 19 commits into master from AD_Ascoli
ADedecker
ADedecker Initial commit
baa51dda
ADedecker Working version!
2d136b55
ADedecker Remove old
1585fd28
ADedecker ADedecker added WIP
ADedecker ADedecker added t-topology
ADedecker ADedecker added t-analysis
ADedecker Only consider things in the union
97960182
ADedecker Change hyp
5c1efc81
ADedecker Begin
713045bd
ADedecker Some progress and experiments
8c1e932f
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 Merge branch 'AD_uniform_convergence_complete' into AD_Ascoli
5682804a
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