continuousAt_coe_iff — Mathlib

English

For x ∈ NNReal and f: ENNReal → α, continuous at ENNReal.ofNNReal x iff continuous at x of f composed with ENNReal.ofNNReal.

Русский

Для x ∈ NNReal и f: ENNReal → α непрерывность в ENNReal.ofNNReal x эквивалентна непрерывности f ∘ ENNReal.ofNNReal в точке x.

LaTeX

$$$\\operatorname{ContinuousAt} f (\\mathrm{ENNReal}.ofNNReal x) \\iff \\operatorname{ContinuousAt} (f \\circ \\mathrm{ENNReal}.ofNNReal) x$$$

Lean4

theorem continuousAt_coe_iff {α : Type*} [TopologicalSpace α] {x : ℝ≥0} {f : ℝ≥0∞ → α} :
    ContinuousAt f ↑x ↔ ContinuousAt (f ∘ (↑) : ℝ≥0 → α) x :=
  tendsto_nhds_coe_iff

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