# mathlibdocumentation

topology.algebra.ordered.extend_from

# Lemmas about extend_from in an order topology. #

theorem continuous_on_Icc_extend_from_Ioo {α : Type u} {β : Type v} [linear_order α] {f : α → β} {a b : α} {la lb : β} (hab : a < b) (hf : (set.Ioo a b)) (ha : (𝓝[] a) (𝓝 la)) (hb : (𝓝[] b) (𝓝 lb)) :
theorem eq_lim_at_left_extend_from_Ioo {α : Type u} {β : Type v} [linear_order α] [t2_space β] {f : α → β} {a b : α} {la : β} (hab : a < b) (ha : (𝓝[] a) (𝓝 la)) :
extend_from (set.Ioo a b) f a = la
theorem eq_lim_at_right_extend_from_Ioo {α : Type u} {β : Type v} [linear_order α] [t2_space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hb : (𝓝[] b) (𝓝 lb)) :
extend_from (set.Ioo a b) f b = lb
theorem continuous_on_Ico_extend_from_Ioo {α : Type u} {β : Type v} [linear_order α] {f : α → β} {a b : α} {la : β} (hab : a < b) (hf : (set.Ioo a b)) (ha : (𝓝[] a) (𝓝 la)) :
theorem continuous_on_Ioc_extend_from_Ioo {α : Type u} {β : Type v} [linear_order α] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hf : (set.Ioo a b)) (hb : (𝓝[] b) (𝓝 lb)) :