limUnder_eq — Mathlib

English

Let f: Y → X be continuous. Then for every y ∈ Y, the limit of f along the neighborhood filter nhds y equals f(y); i.e., limUnder (nhds y) f = f(y).

Русский

Пусть f: Y → X непрерывна. Тогда для каждого y ∈ Y предел f вдоль фильтра окрестностей nhds y равен f(y); то есть limUnder (nhds y) f = f(y).

LaTeX

$$$\\forall y\\in Y,\\ \\limUnder(\\mathcal{N}_y)\\ f = f(y).$$$

Lean4

theorem limUnder_eq [TopologicalSpace Y] {f : Y → X} (h : Continuous f) (y : Y) : @limUnder _ _ _ ⟨f y⟩ (𝓝 y) f = f y :=
  (h.tendsto y).limUnder_eq

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