rpow — Mathlib

English

If f,g are continuous within a set s at x, and at each point x ∈ s we have f(x) ≠ 0 or g(x) > 0, then the function t ↦ f(t)^{g(t)} is continuous within s at x.

Русский

Если F и G непрерывны на s в точке x и для всех x ∈ s выполняется f(x) ≠ 0 или g(x) > 0, то t ↦ f(t)^{g(t)} непрерывна в s и точке x.

LaTeX

$$$$\forall x\in s,\ (f,g)\text{ непрерывны на }s,\ (f(x)\neq 0 \lor g(x) > 0) \Rightarrow \text{ContinuousWithinAt}(t\mapsto f(t)^{g(t)},s,x).$$$$

Lean4

nonrec theorem rpow (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) (h : f x ≠ 0 ∨ 0 < g x) :
    ContinuousWithinAt (fun t => f t ^ g t) s x :=
  hf.rpow hg h

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