zsmul_apply — Mathlib

English

The space of bounded continuous maps α →ᵇ β forms an additive commutative group with the usual pointwise addition and subtraction.

Русский

Множество ограниченных непрерывных отображений образует коммутативную аддитивную группу относительно точечного сложения и вычитания.

LaTeX

$$$\alpha \to^b \beta$ is an AddCommGroup with pointwise operations$$

Lean4

@[simp]
theorem zsmul_apply (r : ℤ) (f : α →ᵇ β) (v : α) : (r • f) v = r • f v :=
  rfl

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