Documentation
Acmoi
.
Exercise1_4
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