Documentation
ExponentialRamsey
.
Prereq
.
Mathlib
.
Data
.
Nat
.
Choose
.
Sum
Search
return to top
source
Imports
Init
Mathlib.Data.Nat.Choose.Sum
Imported by
Nat
.
choose_le_two_pow'
Stuff for data.nat.choose.sum
#
source
theorem
Nat
.
choose_le_two_pow'
{
n
k
:
ℕ
}
:
n
.
choose
k
≤
2
^
n