rpow_const — Mathlib

English

If a function f has compact support and r ≠ 0, then the function x ↦ f(x)^r also has compact support.

Русский

Если функция f имеет компактную опору и r ≠ 0, то функция x ↦ f(x)^r также имеет компактную опору.

LaTeX

$$«Нормальная» формула: HasCompactSupport f → r ≠ 0 → HasCompactSupport (x ↦ f x)^r.$$

Lean4

protected theorem _root_.HasCompactSupport.rpow_const {α : Type*} [TopologicalSpace α] {f : α → ℝ}
    (hf : HasCompactSupport f) {r : ℝ} (hr : r ≠ 0) : HasCompactSupport (fun x ↦ f x ^ r) :=
  hf.comp_left (g := (· ^ r)) (Real.zero_rpow hr)

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