rpow — Mathlib

English

If f,g are continuous on a set s and f(x) ≠ 0 or g(x) > 0 for all x ∈ s, then t ↦ f(t)^{g(t)} is continuous on s.

Русский

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

LaTeX

$$$$\forall t\in s,\ (f(t)\neq 0 \lor g(t) > 0) \Rightarrow \text{ContinuousOn}(t\mapsto f(t)^{g(t)},s).$$$$

Lean4

theorem rpow (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h : ∀ x ∈ s, f x ≠ 0 ∨ 0 < g x) :
    ContinuousOn (fun t => f t ^ g t) s := fun t ht => (hf t ht).rpow (hg t ht) (h t ht)

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