Documentation
ExponentialRamsey
.
Prereq
.
Mathlib
.
Combinatorics
.
SimpleGraph
.
DegreeSum
Search
return to top
source
Imports
Init
Mathlib.Combinatorics.SimpleGraph.DegreeSum
Imported by
SimpleGraph
.
exists_even_degree
Stuff for combinatorics.simple_graph.degree_sum
#
source
theorem
SimpleGraph
.
exists_even_degree
{
V
:
Type
u_1}
{
G
:
SimpleGraph
V
}
[
Fintype
V
]
[
DecidableRel
G
.
Adj
]
(
hV
:
Odd
(
Fintype.card
V
)
)
:
∃ (
v
:
V
),
Even
(
G
.
degree
v
)