ofFun_smul — Mathlib

English

Let 𝔖 be a collection of subsets of α, a scalar c ∈ M, and a function f: α → β. Then applying the operation ofFun 𝔖 to the scaled function c · f yields the same as scaling the result of applying ofFun 𝔖 to f; i.e., ofFun 𝔖 (c · f) = c · ofFun 𝔖 f.

Русский

Пусть 𝔖 — семейство подмножеств α, скаляр c ∈ M и функция f: α → β. Тогда применение операции ofFun 𝔖 к умноженной на константу функции c · f эквивалентно умножению результата: ofFun 𝔖 (c · f) = c · ofFun 𝔖 f.

LaTeX

$$$\mathrm{ofFun}_{\mathfrak{S}}(c \cdot f) = c \cdot \mathrm{ofFun}_{\mathfrak{S}}(f).$$$

Lean4

@[simp]
theorem ofFun_smul {M : Type*} [SMul M β] (c : M) (f : α → β) : ofFun 𝔖 (c • f) = c • ofFun 𝔖 f :=
  rfl

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