pith. machine review for the scientific record. sign in
theorem proved term proof

rpowIntervalSimple_contains_rpow

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  40theorem rpowIntervalSimple_contains_rpow
  41    {result_lo result_hi : ℚ}
  42    (h_valid : result_lo ≤ result_hi)
  43    {x y : ℝ}
  44    (h_lo : (result_lo : ℝ) ≤ x.rpow y)
  45    (h_hi : x.rpow y ≤ (result_hi : ℝ)) :
  46    (rpowIntervalSimple result_lo result_hi h_valid).contains (x.rpow y) :=

proof body

Term-mode proof.

  47  ⟨h_lo, h_hi⟩
  48
  49/-- Interval containing φ = (1 + √5)/2 ≈ 1.618 -/

depends on (5)

Lean names referenced from this declaration's body.