rexp — Mathlib

English

If f is ContinuousWithinAt at x, then exp(f) is ContinuousWithinAt at x.

Русский

Если f непрерывна внутри множества s в точке x, то exp(f) непрерывна внутри множества s в x.

LaTeX

$$$$ \\text{ContinuousWithinAt}(f, s, x) \\Rightarrow \\text{ContinuousWithinAt}(\\exp \\circ f, s, x). $$$$

Lean4

nonrec theorem «rexp» (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun y ↦ exp (f y)) s x :=
  h.rexp

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