mathlib3
feat(combinatorics.simple_graph.metric): `enat` valued dist function on graphs
#18692
Open
Overview
Commits
17
Changes
View On GitHub

feat(combinatorics.simple_graph.metric): `enat` valued dist function on graphs #18692

bottine wants to merge 17 commits into master from bottine/combinatorics.simple_graph.metric/some_lemmas
bottine
bottine init wip
44a0f829
bottine need an enat lemma
ff9f6c02
bottine ok
0723d132
bottine sorried-out lemmas wip
f90758dc
bottine sorried-out lemmas wip
23000845
bottine sorried-out lemmas wip
a3c3f8dd
bottine ok
08fbd414
bottine ok
a2ff284d
bottine closed balls ≠ univ
94d2559b
bottine enough_space_of_transitive
924df91f
bottine closed neighborhood finite
e75a0cce
bottine subset closed neighborhood
0cce40c0
bottine name
2cf40430
bottine lemmas already exist
9c5f16c5
bottine metric space instance
965146b2
bottine merge master
ea313a08
bottine yes
2559d225
bottine bottine requested a review 2 years ago
bottine bottine added WIP
bottine bottine added t-combinatorics
bottine bottine marked this pull request as draft 2 years ago
bottine bottine added t-topology
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 t-topology t-combinatorics too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum