cpow — Mathlib

English

If f and g are ContinuousOn on a set s and f(a) ∈ slitPlane for all a ∈ s, then the map x ↦ f(x)^g(x) is ContinuousOn on s.

Русский

Если f,g непрерывны на s и f(a) ∈ slitPlane для всех a ∈ s, то x ↦ f(x)^g(x) непрерывна на s.

LaTeX

$$$$\\text{If } f,g:\\, s\\to \\mathbb{C},\\ \\text{ContinuousOn } f\\,s,\\ \\text{ContinuousOn } g\\,s,\\ \\forall a\\in s,\\ f(a) \\in \\text{slitPlane} \\Rightarrow \\text{ContinuousOn } (x\\mapsto f(x)^g(x))\\,s.$$$$

Lean4

theorem cpow (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h0 : ∀ a ∈ s, f a ∈ slitPlane) :
    ContinuousOn (fun x => f x ^ g x) s := fun a ha => (hf a ha).cpow (hg a ha) (h0 a ha)

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