∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {s : Set α} [inst_1 : LinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β},
  IsPreconnected s → ContinuousOn f s → (∀ x ∈ s, f x ≠ b) → Set.MapsTo f s (Set.Ioi b) ∨ Set.MapsTo f s (Set.Iio b)