Documentation

Mathlib.Topology.Algebra.Order.ExtendFrom

Lemmas about extendFrom in an order topology. #

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