Documentation

Mathlib.Topology.Algebra.Order.ExtendFrom

Lemmas about extendFrom in an order topology. #

theorem continuousOn_Icc_extendFrom_Ioo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace β] [RegularSpace β] {f : αβ} {a : α} {b : α} {la : β} {lb : β} (hab : a b) (hf : ContinuousOn f (Set.Ioo a b)) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la)) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb)) :
theorem eq_lim_at_left_extendFrom_Ioo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace β] [T2Space β] {f : αβ} {a : α} {b : α} {la : β} (hab : a < b) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la)) :
extendFrom (Set.Ioo a b) f a = la
theorem eq_lim_at_right_extendFrom_Ioo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace β] [T2Space β] {f : αβ} {a : α} {b : α} {lb : β} (hab : a < b) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb)) :
extendFrom (Set.Ioo a b) f b = lb
theorem continuousOn_Ico_extendFrom_Ioo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace β] [RegularSpace β] {f : αβ} {a : α} {b : α} {la : β} (hab : a < b) (hf : ContinuousOn f (Set.Ioo a b)) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la)) :
theorem continuousOn_Ioc_extendFrom_Ioo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace β] [RegularSpace β] {f : αβ} {a : α} {b : α} {lb : β} (hab : a < b) (hf : ContinuousOn f (Set.Ioo a b)) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb)) :