const_fun_smul — Mathlib

English

If f is CircleIntegrable, then the function z ↦ a • f(z) is CircleIntegrable.

Русский

Если f CircleIntegrable, то z ↦ a • f(z) CircleIntegrable.

LaTeX

$$$\text{CircleIntegrable}(f,c,R) \Rightarrow \text{CircleIntegrable}(\,z \mapsto a \cdot f(z)\,, c,R).$$$

Lean4

/-- If `f` is circle integrable, then so are its scalar multiples. -/
theorem const_fun_smul {f : ℂ → A} (h : CircleIntegrable f c R) : CircleIntegrable (fun z ↦ a • f z) c R :=
  const_smul h

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