mpullbackWithin_smul_apply — Mathlib

English

For any scalar c and vector fields V, mpullbackWithin I I' f (c·V) s x = c · mpullbackWithin I I' f V s x.

Русский

Для любого скаляра c и полей векторов выполняется равенство: mpullbackWithin I I' f (c·V) s x = c · mpullbackWithin I I' f V s x.

LaTeX

$$$$ \mathrm{mpullbackWithin}\ I\ I'\ f\ (c\cdot V)\ s\ x = c\cdot \mathrm{mpullbackWithin}\ I\ I'\ f\ V\ s\ x $$$$

Lean4

theorem mpullbackWithin_smul_apply : mpullbackWithin I I' f (c • V) s x = c • mpullbackWithin I I' f V s x := by
  simp [mpullbackWithin_apply]

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