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

smulPos_contains_smul

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)

 133theorem smulPos_contains_smul {q : ℚ} {x : ℝ} {I : Interval}
 134    (hq : 0 < q) (hx : I.contains x) : (smulPos q I hq).contains ((q : ℝ) * x) := by

proof body

Tactic-mode proof.

 135  have hq_pos : (0 : ℝ) < q := by exact_mod_cast hq
 136  constructor
 137  · simp only [smulPos, Rat.cast_mul]
 138    exact mul_le_mul_of_nonneg_left hx.1 (le_of_lt hq_pos)
 139  · simp only [smulPos, Rat.cast_mul]
 140    exact mul_le_mul_of_nonneg_left hx.2 (le_of_lt hq_pos)
 141
 142/-- Power by natural number for positive intervals -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.