continuous_iff'_right — Mathlib

English

Continuous f is characterized by Tendsto (f b, f x) for all b into the uniformity.

Русский

Непрерывность f эквивалентна Tendsto (f b, f x) для всех b в 𝓤 α.

LaTeX

$$$\\operatorname{Continuous}(f) \\iff \\forall b, \\operatorname{Tendsto}(f b, f x) (\\mathcal{N} b) (𝓤 α)$$$

Lean4

theorem continuous_iff'_right [TopologicalSpace β] {f : β → α} :
    Continuous f ↔ ∀ b, Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α) :=
  continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_right

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