fourierPowSMulRight — Mathlib

English

If f is continuous, then the map v ↦ fourierPowSMulRight L f v n is continuous in v for every fixed n.

Русский

Если f непрерывна, то v ↦ fourierPowSMulRight L f v n непрерывна по v при любом фиксированном n.

LaTeX

$$$\\text{Continuous}(v \\mapsto \\text{fourierPowSMulRight } L f v n)$$$

Lean4

@[continuity, fun_prop]
theorem _root_.Continuous.fourierPowSMulRight {f : V → E} (hf : Continuous f) (n : ℕ) :
    Continuous (fun v ↦ fourierPowSMulRight L f v n) :=
  by
  simp_rw [fourierPowSMulRight_eq_comp]
  apply Continuous.const_smul
  apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp₂ _ hf
  exact Continuous.comp (map_continuous _) (continuous_pi (fun _ ↦ L.continuous))

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