# mathlib3documentation

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} [linear_order α] {f : α β} {a b : α} {la lb : β} (hab : a b) (hf : (set.Ioo a b)) (ha : (set.Ioi a)) (nhds la)) (hb : (set.Iio b)) (nhds 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 : (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} [linear_order α] [t2_space β] {f : α β} {a b : α} {lb : β} (hab : a < b) (hb : (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} [linear_order α] {f : α β} {a b : α} {la : β} (hab : a < b) (hf : (set.Ioo a b)) (ha : (set.Ioi a)) (nhds 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 : (set.Iio b)) (nhds lb)) :