Documentation
Acmoi
.
Exercise1_4
Search
Google site search
return to top
source
Imports
Init
Mathlib.Tactic.Ring
Mathlib.Data.Real.Basic
Imported by
SW_15_induction
source
theorem
SW_15_induction
(x :
ℝ
)
(k :
ℕ
)
(h0 :
0
≤
x
)
(h1 :
x
≤
1
)
:
1
-
↑
k
*
x
≤
(
1
-
x
)
^
k