ereal_toENNReal — Mathlib

English

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

Русский

Если f непрерывна в отношении множества s в точке x, тогда x ↦ (f(x)).toENNReal непрерывна в отношении s в x.

LaTeX

$$$ ContinuousWithinAt f s x \Rightarrow ContinuousWithinAt (\lambda x. (f x).toENNReal) s x $$$

Lean4

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

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