leanprover-community/mathlib

Pull Requests Commits
F-H.lean ported
bottine committed 3 years ago
25687c25
finish porting ends_limit_construction.lean
bottine committed 3 years ago
6d960186
kill the commas
bottine committed 3 years ago
ac2dbf21
advances in porting ends_limit_construction.lean
bottine committed 3 years ago
52aaec04
some tweaks in FH
bottine committed 3 years ago
3336a60a
some tweaks
bottine committed 3 years ago
fe756712
one sorry
bottine committed 3 years ago
493142c5
Finish `CompOut` surjectivity proof
0art0 committed 3 years ago
cc193b5f
bit of a cleanup
bottine committed 3 years ago
f7d5131a
bit of a cleanup
bottine committed 3 years ago
78f30df1
roadblock uglily overcome
bottine committed 3 years ago
2da38e48
roadblock F-H
bottine committed 3 years ago
17babcf8
some sorrys removed, lots added
bottine committed 3 years ago
a55209cc
reorg for F-H
bottine committed 3 years ago
2cd55896
Merge branch 'bottine/simple_graph_ends' of https://github.com/bottine/mathlib into bottine/simple_graph_ends
0art0 committed 3 years ago
0f70065a
Induction on infinite components
0art0 committed 3 years ago
96ebd7da
dirty commit
bottine committed 3 years ago
3035fb0d
hopefully a successful merge
bottine committed 3 years ago
c1a00d90
Progress on the isomorphism
0art0 committed 3 years ago
ceab7134
inf_iff_surjective wip
bottine committed 3 years ago
7cb8b1aa
details
bottine committed 3 years ago
fc1a4c9c
define the ends functors, _again_
bottine committed 3 years ago
31f13771
start porting Hopf-Freudenthal
bottine committed 3 years ago
7223f771
nicely arranged (probbly easily shortened with fewer by_contra and by_cases)
bottine committed 3 years ago
8cfa1c26
little lemmas
bottine committed 3 years ago
b57d7d95
Some progress
0art0 committed 3 years ago
616717aa
equiv_of_isom for comp_out
bottine committed 3 years ago
a1ebb23c
Merge branch 'bottine/simple_graph_ends' of ssh://github.com/bottine/mathlib into bottine/simple_graph_ends
bottine committed 3 years ago
afd76554
mostly stubs
bottine committed 3 years ago
920ed59a
Minor cleanup and changes
0art0 committed 3 years ago
ae3149a9
Terms Of Use Privacy Policy Refund Policy Impressum