smul — Mathlib

English

For any filtration f and value x in β, the constant function with value x is adapted.

Русский

Для произвольной фильтрации f и значения x в β константная функция со значением x адаптирована.

LaTeX

$$$$ \\mathrm{Adapted}(f, \\text{const}_x) $$$$

Lean4

protected theorem smul [SMul ℝ β] [ContinuousConstSMul ℝ β] (c : ℝ) (hu : Adapted f u) : Adapted f (c • u) := fun i =>
  (hu i).const_smul c

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