lean_workbook_plus_38218
ProvedNote that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38218 (x : ℝ) (n : ℕ) : x ∈ Set.Icc 0 1 → x ^ (n + 1) ≤ x ^ n := by sorry
Source
Note that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38218 (x : ℝ) (n : ℕ) : x ∈ Set.Icc 0 1 → x ^ (n + 1) ≤ x ^ n := by sorry