English
There is a continuous extension from Ioo to Icc that preserves left-right continuity under appropriate assumptions.
Русский
Существует непрерывное продолжение из Ioo в Icc, сохраняющее левую и правую непрерывность при соответствующих предположениях.
LaTeX
$$$\\text{ContinuousOn}(\\operatorname{extendFrom}(Ioo(a,b),f), Icc(a,b)).$$$
Lean4
theorem continuousOn_Ioc_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α]
[TopologicalSpace β] [RegularSpace β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : ContinuousOn f (Ioo a b))
(hb : Tendsto f (𝓝[<] b) (𝓝 lb)) : ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b) :=
by
have := @continuousOn_Ico_extendFrom_Ioo αᵒᵈ _ _ _ _ _ _ _ f _ _ lb hab
erw [Ico_toDual, Ioi_toDual, Ioo_toDual] at this
exact this hf hb
