distribSMulSet — Mathlib

English

If β is an additive monoid and α distributes over β (DistribSMul), then the induced action on sets distributes over the set addition: a • (X + Y) = (a • X) + (a • Y).

Русский

Если β — аддитивный моноид и α действует распределительно на β (DistribSMul), то и на множествах выполняется распределение над суммой: a • (X + Y) = (a • X) + (a • Y).

LaTeX

$$$ a \cdot (X \oplus Y) = (a \cdot X) \oplus (a \cdot Y) $$$

Lean4

/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
then so is `(· • ·) : α → Set β → Set β`. -/
protected noncomputable def distribSMulSet [AddZeroClass β] [DistribSMul α β] : DistribSMul α (Set β) where
  smul_add _ _ _ := image_image2_distrib <| smul_add _

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