ereal_toENNReal — Mathlib

English

If f is continuous at a point x, then x ↦ (f(x)).toENNReal is continuous at x.

Русский

Если f непрерывна в точке x, то x ↦ (f(x)).toENNReal непрерывна в точке x.

LaTeX

$$$ ContinuousAt f x \Rightarrow ContinuousAt (\lambda x. (f x).toENNReal) x $$$

Lean4

@[fun_prop]
theorem _root_.ContinuousAt.ereal_toENNReal {α : Type*} [TopologicalSpace α] {f : α → EReal} {x : α}
    (hf : ContinuousAt f x) : ContinuousAt (fun x => (f x).toENNReal) x :=
  continuous_toENNReal.continuousAt.comp hf

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