def
definition
def or abbrev
expIntervalSimple
show as:
view Lean formalization →
formal statement (Lean)
32def expIntervalSimple (I : Interval) (hI_lo : 0 ≤ I.lo) (hI_hi : I.hi < 1) : Interval where
33 lo := expLowerSimple I.lo
proof body
Definition body.
34 hi := expUpperSimple I.hi
35 valid := by
36 simp only [expLowerSimple, expUpperSimple]
37 have h_denom_pos : 0 < 1 - I.hi := by linarith
38 have h1 : I.lo + 1 ≤ I.hi + 1 := by linarith [I.valid]
39 have h2 : I.hi + 1 ≤ 1 / (1 - I.hi) := by
40 rw [le_div_iff₀ h_denom_pos]
41 ring_nf
42 nlinarith [sq_nonneg I.hi, I.valid]
43 linarith
44