eq_lim_at_left_extendFrom_Ioo — Mathlib

English

If a < b and f has left-hand limit la along the right-neighborhood of a, then the extension from Ioo to a equals la at a.

Русский

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

LaTeX

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

Lean4

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

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