Theorem: exercise6_4 (LeanCourse/Assignments/Assignment6.lean)

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → α
hf : Continuous f
h2f : Injective f
a b : α
hab : a ≤ b
h2ab : f a < f b
⊢ StrictMonoOn f (Ici a)
Tactic:
sorry
State after:
no goals