const_smul — Mathlib

English

If f is CircleIntegrable, then a • f is CircleIntegrable for any scalar a in the underlying ring.

Русский

Если f CircleIntegrable, то a • f CircleIntegrable для любого скаляра a.

LaTeX

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

Lean4

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

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