leanprover-community/mathlib

Pull Requests Commits
Make `connected_component`s more set-like
0art0 committed 3 years ago
fff77402
structure for inf and dis comps
bottine committed 3 years ago
14830881
little things
bottine committed 3 years ago
6d9bc446
exists infinite comp
bottine committed 3 years ago
3bb71f72
back of dis is dis (iow: C.back is disjoint ffrom its base set if C is disjoint from its base set)
bottine committed 3 years ago
98d88133
infinite iff surjective first troubles
bottine committed 3 years ago
16cbdeba
finiteness of comp_out
bottine committed 3 years ago
44c4c726
more lemmas in comp_out.lean
bottine committed 3 years ago
529b9661
Complete proof with `simple_graph.walk.map`
0art0 committed 3 years ago
6dc8762f
A connected set is contained in a conn component
0art0 committed 3 years ago
ad380ea1
one lemma with nicer proof?
bottine committed 3 years ago
d848e0d2
alternative path for comp_out
bottine committed 3 years ago
c2bd8b43
dirty commit
bottine committed 3 years ago
9d93eb46
one more lemma
bottine committed 3 years ago
05c4eb4e
connected_supp
bottine committed 3 years ago
70c3f8a0
and forgot a file
bottine committed 3 years ago
9b7e7ae3
few lemmas out
bottine committed 3 years ago
071b920c
lemma stubs
bottine committed 3 years ago
da43aaec
Define subtype functor and related lemmas
0art0 committed 3 years ago
56b8d6dc
dirty
bottine committed 3 years ago
25d838f3
set_like for conn_comp_outside
bottine committed 3 years ago
d4ccdb7f
coercion for conn_comp_outside ?
bottine committed 3 years ago
b8180df8
Porting Freudenthal-Hopf first steps
bottine committed 3 years ago
92fc4478
Add lemmas about `ComplInfComp`
0art0 committed 3 years ago
ef95a2f5
subfunctor.ext by Adam Topaz
bottine committed 3 years ago
41d3e176
Change `surjective'` to `surjective`
0art0 committed 3 years ago
f2aa8ce4
Shorten `subfunctor.ext` proof
0art0 committed 3 years ago
f7715cca
Subfunctor surjectivity
0art0 committed 3 years ago
11c57c80
add subfunctor code
bottine committed 3 years ago
99d774ba
Merge branch 'bottine/simple_graph_ends' of ssh://github.com/bottine/mathlib into bottine/simple_graph_ends
bottine committed 3 years ago
36073bdd
Terms Of Use Privacy Policy Refund Policy Impressum