English
If f is continuous on the open interval Ioo(a,b) in a densely ordered space with order topology, and the one-sided limits at a and b exist, then the natural extension to the closed interval Icc(a,b) is continuous there.
Русский
Если f непрерывна на открытом интервале Ioo(a,b) в плотном упорядоченном пространстве с топологией порядка, и существуют односторонние пределы в точках a и b, то естественное продолжение до закрытого интервала Icc(a,b) непрерывно там.
LaTeX
$$$f$ непрерывно на $Ioo(a,b)$, пределы в левой и правой границе существуют; тогда продолжение $\\operatorname{extendFrom}(Ioo(a,b),f)$ непрерывно на $Icc(a,b)$.$$
Lean4
theorem continuousOn_Icc_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α]
[TopologicalSpace β] [RegularSpace β] {f : α → β} {a b : α} {la lb : β} (hab : a ≠ b)
(hf : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 la)) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) :
ContinuousOn (extendFrom (Ioo a b) f) (Icc a b) :=
by
apply continuousOn_extendFrom
· rw [closure_Ioo hab]
· intro x x_in
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
· exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
· exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
· exact ⟨f x, hf x h⟩
