theorem proved term proof

`faster_contraction_faster_thinking`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  88theorem faster_contraction_faster_thinking (c₁ c₂ : ℝ)
  89    (h₁ : 0 < c₁) (h₂ : 0 < c₂)
  90    (h_faster : c₁ < c₂) (error : ℝ) (he : 0 < error) (n : ℕ) :
  91    c₁ ^ n * error ≤ c₂ ^ n * error := by

proof body

Term-mode proof.

  92  apply mul_le_mul_of_nonneg_right
  93  · exact pow_le_pow_left₀ (le_of_lt h₁) (le_of_lt h_faster) n
  94  · exact le_of_lt he
  95
  96end IndisputableMonolith.Foundation.RHatFixedPoint