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

mulPos_contains_mul

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)

 113theorem mulPos_contains_mul {x y : ℝ} {I J : Interval}
 114    (hIpos : 0 < I.lo) (hJpos : 0 < J.lo)
 115    (hx : I.contains x) (hy : J.contains y) : (mulPos I J hIpos hJpos).contains (x * y) := by

proof body

Tactic-mode proof.

 116  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
 117  have hJlo_pos : (0 : ℝ) < J.lo := by exact_mod_cast hJpos
 118  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
 119  have hy_pos : 0 < y := lt_of_lt_of_le hJlo_pos hy.1
 120  have hIhi_pos : (0 : ℝ) ≤ I.hi := le_trans (le_of_lt hIlo_pos) (by exact_mod_cast I.valid)
 121  constructor
 122  · simp only [mulPos, Rat.cast_mul]
 123    exact mul_le_mul hx.1 hy.1 (le_of_lt hJlo_pos) (le_trans (le_of_lt hIlo_pos) hx.1)
 124  · simp only [mulPos, Rat.cast_mul]
 125    exact mul_le_mul hx.2 hy.2 (le_of_lt hy_pos) hIhi_pos
 126
 127/-- Scalar multiplication by a positive rational -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.