mathlib3 documentation

topology.algebra.order.extend_from

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)) :
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)) :
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)) :