English
There is a continuous extension from Ioo to Icc that is well-behaved on the left endpoint set Ico.
Русский
Существует непрерывное продолжение из Ioo в Icc, согласующееся с левой границей на Ico.
LaTeX
$$$\\text{ContinuousOn}(\\operatorname{extendFrom}(Ioo(a,b),f), Ico(a,b)).$$$
Lean4
theorem continuousOn_Ico_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α]
[TopologicalSpace β] [RegularSpace β] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : ContinuousOn f (Ioo a b))
(ha : Tendsto f (𝓝[>] a) (𝓝 la)) : ContinuousOn (extendFrom (Ioo a b) f) (Ico a b) :=
by
apply continuousOn_extendFrom
· rw [closure_Ioo hab.ne]
exact Ico_subset_Icc_self
· intro x x_in
rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)
· use la
simpa [hab]
· exact ⟨f x, hf x h⟩
