continuousAt_iff_prod — Mathlib

English

For f: β → α, the product tendsto criterion characterizes pointwise convergence by pairing arguments.

Русский

Критерий суммарной сходимости через пару аргументов описывает точечную непрерывность.

LaTeX

$$$\\text{continuousAt}_{\\text{prod}}(f,b) \\iff \\operatorname{Tendsto} (\\lambda (x,y). (f x, f y)) (\\mathcal{N}(b, b)) (𝓤 α)$$$

Lean4

theorem continuousAt_iff_prod [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAt f b ↔ Tendsto (fun x : β × β => (f x.1, f x.2)) (𝓝 (b, b)) (𝓤 α) :=
  ⟨fun H => le_trans (H.prodMap' H) (nhds_le_uniformity _), fun H =>
    continuousAt_iff'_left.2 <| H.comp <| tendsto_id.prodMk_nhds tendsto_const_nhds⟩

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