const_cpow — Mathlib

English

The map x ↦ b^f(x) is continuous within a if f is continuous within a and either b ≠ 0 or f(a) ≠ 0.

Русский

Если f непрерывна в рамках s в точке a, и либо b ≠ 0, либо f(a) ≠ 0, тогда функция x ↦ b^{f(x)} непрерывна в рамках s в a.

LaTeX

$$ContinuousWithinAt (fun x => b ^ f x) s a$$

Lean4

nonrec theorem const_cpow {b : ℂ} (hf : ContinuousWithinAt f s a) (h : b ≠ 0 ∨ f a ≠ 0) :
    ContinuousWithinAt (fun x => b ^ f x) s a :=
  hf.const_cpow h

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