Lemmas about extend_from in an order topology. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
continuous_on_Icc_extend_from_Ioo
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[densely_ordered α]
[order_topology α]
[topological_space β]
[regular_space β]
{f : α → β}
{a b : α}
{la lb : β}
(hab : a ≠ b)
(hf : continuous_on f (set.Ioo a b))
(ha : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds la))
(hb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds lb)) :
continuous_on (extend_from (set.Ioo a b) f) (set.Icc a b)
theorem
eq_lim_at_left_extend_from_Ioo
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[densely_ordered α]
[order_topology α]
[topological_space β]
[t2_space β]
{f : α → β}
{a b : α}
{la : β}
(hab : a < b)
(ha : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds la)) :
extend_from (set.Ioo a b) f a = la
theorem
eq_lim_at_right_extend_from_Ioo
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[densely_ordered α]
[order_topology α]
[topological_space β]
[t2_space β]
{f : α → β}
{a b : α}
{lb : β}
(hab : a < b)
(hb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds lb)) :
extend_from (set.Ioo a b) f b = lb
theorem
continuous_on_Ico_extend_from_Ioo
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[densely_ordered α]
[order_topology α]
[topological_space β]
[regular_space β]
{f : α → β}
{a b : α}
{la : β}
(hab : a < b)
(hf : continuous_on f (set.Ioo a b))
(ha : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds la)) :
continuous_on (extend_from (set.Ioo a b) f) (set.Ico a b)
theorem
continuous_on_Ioc_extend_from_Ioo
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order α]
[densely_ordered α]
[order_topology α]
[topological_space β]
[regular_space β]
{f : α → β}
{a b : α}
{lb : β}
(hab : a < b)
(hf : continuous_on f (set.Ioo a b))
(hb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds lb)) :
continuous_on (extend_from (set.Ioo a b) f) (set.Ioc a b)