mathlib documentation

topology.algebra.ordered.extend_from

Lemmas about extend_from in an order topology. #

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 (𝓝[set.Ioi a] a) (𝓝 la)) (hb : filter.tendsto f (𝓝[set.Iio b] b) (𝓝 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 (𝓝[set.Ioi a] a) (𝓝 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 (𝓝[set.Iio b] b) (𝓝 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 (𝓝[set.Ioi a] a) (𝓝 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 (𝓝[set.Iio b] b) (𝓝 lb)) :