Theorem: exercise6_3 (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 x : α
hab : a ≤ b
h2ab : f a < f b
hx : a ≤ x
⊢ f a ≤ f x
Tactic:
sorry
State after:
no goals