Lemmas about extendFrom in an order topology. #
theorem
continuousOn_Icc_extendFrom_Ioo
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[DenselyOrdered α]
[OrderTopology α]
[TopologicalSpace β]
[RegularSpace β]
{f : α → β}
{a b : α}
{la lb : β}
(hab : a ≠ b)
(hf : ContinuousOn f (Set.Ioo a b))
(ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la))
(hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb))
:
ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Icc a b)
theorem
eq_lim_at_left_extendFrom_Ioo
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[DenselyOrdered α]
[OrderTopology α]
[TopologicalSpace β]
[T2Space β]
{f : α → β}
{a b : α}
{la : β}
(hab : a < b)
(ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la))
:
extendFrom (Set.Ioo a b) f a = la
theorem
eq_lim_at_right_extendFrom_Ioo
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[DenselyOrdered α]
[OrderTopology α]
[TopologicalSpace β]
[T2Space β]
{f : α → β}
{a b : α}
{lb : β}
(hab : a < b)
(hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb))
:
extendFrom (Set.Ioo a b) f b = lb
theorem
continuousOn_Ico_extendFrom_Ioo
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[DenselyOrdered α]
[OrderTopology α]
[TopologicalSpace β]
[RegularSpace β]
{f : α → β}
{a b : α}
{la : β}
(hab : a < b)
(hf : ContinuousOn f (Set.Ioo a b))
(ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la))
:
ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Ico a b)
theorem
continuousOn_Ioc_extendFrom_Ioo
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[DenselyOrdered α]
[OrderTopology α]
[TopologicalSpace β]
[RegularSpace β]
{f : α → β}
{a b : α}
{lb : β}
(hab : a < b)
(hf : ContinuousOn f (Set.Ioo a b))
(hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb))
:
ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Ioc a b)