lean_workbook_plus_64739
ProvedUse induction to show for all real number and all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64739 (n : ℕ) (x : ℝ) (hx: x ≤ 1) : (1 - x)^n ≥ 1 - n*x := by sorry
Source
Use induction to show for all real number and all .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_64739 (n : ℕ) (x : ℝ) (hx: x ≤ 1) : (1 - x)^n ≥ 1 - n*x := by sorry