rpow_const — Mathlib

English

If f is continuous within s at x and f(x) ≠ 0 or p ≥ 0, then x ↦ f(x)^p is continuous within s at x.

Русский

Если f непрерывна внутри s в точке x и f(x) ≠ 0 или p ≥ 0, то x ↦ f(x)^p непрерывна внутри s в x.

LaTeX

$$$$\text{ContinuousWithinAt}(f,s,x) \land (f(x)\neq 0 \lor p\ge 0) \Rightarrow \text{ContinuousWithinAt}(t\mapsto f(t)^p,s,x).$$$$

Lean4

nonrec theorem rpow_const (hf : ContinuousWithinAt f s x) (h : f x ≠ 0 ∨ 0 ≤ p) :
    ContinuousWithinAt (fun x => f x ^ p) s x :=
  hf.rpow_const h

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