rpow — Mathlib

English

Same as above; the rpow operation preserves continuity on a set when the pointwise condition holds.

Русский

То же самое; операция rpow сохраняет непрерывность на множестве при выполнении условия по точкам.

LaTeX

$$$$\text{ContinuousOn}((f,g),s) \Rightarrow \ ext{ContinuousOn}(t\mapsto f(t)^{g(t)},s) \text{ при } \forall x\in s, f(x)\neq0 \lor 0< g(x).$$$$

Lean4

theorem rpow (hf : Continuous f) (hg : Continuous g) (h : ∀ x, f x ≠ 0 ∨ 0 < g x) : Continuous fun x => f x ^ g x :=
  continuous_iff_continuousAt.2 fun x => hf.continuousAt.rpow hg.continuousAt (h x)

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