∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : TopologicalSpace α] [OrderTopology α]
  [inst_4 : LinearOrder β] [WellFoundedLT β] [inst_6 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Order.IsNormal f → Continuous f