mathlib3
feat(combinatorics.simple_graph.ends): A version of Freudenthal-Hopf
#18681
Open
Overview
Commits
149
Changes
View On GitHub

feat(combinatorics.simple_graph.ends): A version of Freudenthal-Hopf #18681

bottine wants to merge 149 commits into master from bottine/simple_graph.ends/Freudenthal_Hopf
bottine
bottine merge
2529a2c0
bottine cleanup?
b7d462df
bottine inf_comp_out
812364d2
bottine Update src/combinatorics/simple_graph/ends/defs.lean
fb3f2f8c
bottine cosmetic
baecb969
bottine docstrings
0d1b4c38
0art0 Expand subtype in `out_hom` and golf proofs
b751399b
0art0 Merge branch 'bottine/simple_graph/ends_for_real_this_time' of https:…
55ebf1f6
0art0 Erase `diff` artefact
7b09ed3a
bottine finite graphs have no end
78ab79c4
bottine docstring
69b305ac
bottine Apply suggestions from code review
88965289
bottine errors
3dc91f19
bottine errors'
2f59b641
bottine op
9b8fca74
bottine Update src/combinatorics/simple_graph/ends/properties.lean
74a79df2
bottine comp_out.hom reverse order and error
b2e5f0a7
bottine better names
bc7b6ed1
bottine Yael's suggestion
565868a5
bottine forgot this
9f4c2848
bottine Apply suggestions from code review
72f20848
bottine Kyle's suggestions
11f0d5be
0art0 Update src/combinatorics/simple_graph/ends/defs.lean
1829b622
bottine Kyle's suggestions
fbc6a777
bottine a few lemmas + tweaks
bd191026
bottine some golf
372a4093
bottine some of Yael's suggestions
8fcdc886
bottine better
9f616856
bottine tweaks
4f2d83fa
bottine Yael's suggestions
155b3c72
bottine details
e7b62ee1
bottine Yael's suggestions
e3ae43f4
bottine Update src/combinatorics/simple_graph/ends/defs.lean
06da513f
bottine Update src/combinatorics/simple_graph/ends/defs.lean
8e846e7f
bottine minor
236853e7
bottine Merge branch 'bottine/simple_graph/ends_for_real_this_time' of ssh://…
cca1fd9b
bottine Junyan's suggestions
dd4cbb98
bottine Merge remote-tracking branch 'origin/master' into bottine/simple_grap…
4771281b
bottine Junyan's suggestions
a8af6ee9
bottine s/comp_out/component_compl/g
39286e4b
bottine some of Junyan's suggestions
0b6aa5dd
bottine Update src/combinatorics/simple_graph/ends/defs.lean
fcf0adb3
bottine init.
9521fd01
bottine move lemma
d97693d9
bottine fix
4c2c380d
bottine comment
ec832745
bottine moved lemma
d5456ac6
bottine merge
39f7b3fa
bottine merge+
539c5326
bottine minigolf
8d0384e8
bottine dirty commit
824214fc
bottine dirty commit
54e66ced
bottine very dirty commit
3bcaef4d
bottine sorrys
e1792aae
bottine Yael's suggestions
f4704ff1
bottine Update defs.lean
b205093a
bottine Update src/combinatorics/simple_graph/ends/defs.lean
73b8774a
bottine dunno
ddad038f
0art0 Prove `induce_induce`
e05965e5
0art0 `induce_induce` code clean-up
62c6b357
bottine messy
250544e6
bottine a lemma
48c3c4e9
bottine Merge branch 'bottine/simple_graph.ends/Freudenthal_Hopf' of ssh://gi…
dd0ba7d6
bottine minigolf
af6e1c9e
bottine move lemma
6b37b93c
bottine use lemma
335d6a51
bottine wip
430233af
bottine wip
30275452
bottine yael's suggestion
e7333179
bottine minigolf
d05508c8
bottine lemmaization
3d873916
bottine cleaner sorrys
8968617a
bottine more better sorrys
e0ecbcd7
bottine minigolf
186e0099
bottine mimniganiset
742ccd65
bottine minigolf''
c9196845
bottine suite
a4090528
bottine wip
ba8ef5f5
bottine wip
acdd33a1
bottine wip
003b6d30
bottine suite
42b6fef4
bottine dirty
ff34a50c
bottine wip mittag_leffler
fe3a90ae
bottine wip m-l
2ed19fa2
bottine m-l cleanup
9849ea00
bottine m-l cleanup
34d0d567
bottine sorry--
8040dbc6
bottine minor
76c243e6
bottine minor
02f99140
bottine skeletal lemma
44c2edc7
bottine lowol
aec958c3
bottine lowowowl
c64bf26c
bottine wip
dff8a5e9
bottine wip file added
525fb02d
bottine starting with the 'extension' lemma
7158ca91
0art0 Reorganise according to new plan
ebaf876f
0art0 Proofs of various properties
2ac8418f
bottine wip
639c77bf
0art0 Prove `induce.iso`
20f4fc75
0art0 Proof of `iso_equiv_supp`
fbd82999
bottine yeah
58f7b960
bottine no
bf4afb13
bottine wip
5101d357
bottine wip
3dc5be02
bottine wip
19fd06e8
bottine Merge branch 'bottine/simple_graph.ends/Freudenthal_Hopf' of ssh://gi…
5b138132
bottine clean
c30139ac
bottine renamings
72824a94
bottine low
ad5f9e8a
bottine init
4abf56aa
bottine yes
3977cc56
bottine better
16fcab70
bottine space after commas
502c9ad8
bottine ok
9399714b
bottine typo
62eaba59
bottine typo
12dbe1b4
bottine partial work after Kyle's review
3986b45a
bottine partial work after Kyle's review
3a3d7c4e
bottine more
fabcf955
bottine one less import
d18b7cc4
bottine move bits from connectivity.lean
069906f1
bottine more
a91a7bc3
bottine more
8f233792
bottine better lattice defs
d0b649cb
bottine remove complete lattice and patches for subgraphs
fecee1f6
bottine yael's suggestion plus one lemma
98a1b204
bottine Remove `induce_singleton_connected`
c1583412
bottine code review
27b5099b
bottine nonempty and finite instances for `component_compl_functor`
d9385949
bottine misc
96e927fc
bottine Merge remote-tracking branch 'origin/master' into bottine/simple_grap…
df3dc4a3
bottine merge master and code review
301524d3
bottine forgot to propagate change
9adbcdc3
bottine Kyle's reviews and snippets
2abf2eba
bottine Merge branch 'master' into bottine/combinatorics.simple_graph.connect…
d4e65696
bottine errors
eba15f7f
bottine merge origin/master
bbec9ee3
bottine merge a pr
07d71f7e
bottine trying to clean things up
e1223d23
bottine another branch
28efb97a
bottine dirty commit
d9ff68a9
bottine cleaner basis
a42e417c
bottine wip
0ee54229
bottine wip
2440632e
bottine wip
a1dd7cff
bottine wip
66ebe530
bottine typechecks
ebac906f
bottine bottine added WIP
bottine bottine added t-combinatorics
bottine bottine requested a review 2 years ago
bottine bottine marked this pull request as draft 2 years ago
bottine wip
a0a12ce6
bottine removed unused file
81d28e15
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
mathlib-dependent-issues-bot
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
WIP blocked-by-other-PR t-combinatorics too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum