E : Type ?u.412812
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.412908
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y
E : Type ?u.412812
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.412908
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x
⊢ StrictMonoOn f D
intro x hx y hy
E : Type ?u.412812
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.412908
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
this : DifferentiableOn ℝ f (interior D)
⊢ x < y → f x < f y
E : Type ?u.412812
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.412908
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y
have : DifferentiableOn ℝ f (interior D) := fun z hz =>
  (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').differentiableWithinAt
no goals
E : Type ?u.412812
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.412908
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ (x : ℝ), x ∈ interior D → 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
this : DifferentiableOn ℝ f (interior D)
⊢ x < y → f x < f y
simpa only [zero_mul, sub_pos] using
  hD.mul_sub_lt_image_sub_of_lt_deriv hf this hf' x hx y hy