Intervals in order topologies

An unordered closed interval is a neighbourhood of each of its points other than its endpoints.

The image of a half-infinite real interval under a continuous strictly monotone map is determined by its value at the finite endpoint and its limit at infinity. The endpoint at infinity is omitted when the limit is finite.

Main results

• TauCeti.uIcc_mem_nhds_of_ne — uIcc a b is a neighbourhood of each of its points other than a and b.
• ContinuousOn.image_Ici_of_strictMonoOn_of_tendsto — a continuous strictly increasing map on Ici p with a finite limit at +∞ maps that interval to the half-open interval between its endpoint value and its limit.

theorem TauCeti.uIcc_mem_nhds_of_ne {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b t : α} (ht : t ∈ Set.uIcc a b) (ha : t ≠ a) (hb : t ≠ b) : Set.uIcc a b ∈ nhds t

An unordered closed interval uIcc a b is a neighbourhood of each of its points other than its endpoints a and b.

theorem ContinuousOn.image_Ici_of_strictMonoOn_of_tendsto {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {d : α → β} {p : α} {D : β} (hdcont : ContinuousOn d (Set.Ici p)) (hdmono : StrictMonoOn d (Set.Ici p)) (hdl : Filter.Tendsto d Filter.atTop (nhds D)) : d '' Set.Ici p = Set.Ico (d p) D

A continuous strictly increasing map sends a half-line to a half-open interval. The finite limit at +∞ is approached but is not attained.