eq_lim_at_right_extendFrom_Ioo — Mathlib

English

If a < b and a right-hand limit at b exists, then the extension from Ioo to b equals lb at b.

Русский

Если a < b и у функции f существует предел слева в точке b, то продолжение от Ioo до b дает значение lb в точке b.

LaTeX

$$$\\extendFrom(Ioo(a,b),f)(b)=lb$ under the given limit condition.$$

Lean4

theorem eq_lim_at_right_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α]
    [TopologicalSpace β] [T2Space β] {f : α → β} {a b : α} {lb : β} (hab : a < b) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) :
    extendFrom (Ioo a b) f b = lb := by
  apply extendFrom_eq
  · rw [closure_Ioo hab.ne]
    simp only [le_of_lt hab, right_mem_Icc]
  · simpa [hab]

Похожие утверждения