∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [Topology.IsUpperSet α] [Topology.IsUpper β] {f : α → β}, Monotone f → Continuous f