image_op_smul_distrib — Mathlib

English

The image under op-smul distributes similarly with a function: f '' (s <• a) = f '' s <• f a.

Русский

Образ под op-smul распределяется: f '' (s <• a) = f '' s <• f a.

LaTeX

$$$ f '' (s <\u2021 a) = f '' s <\u2021 f a $$$

Lean4

@[to_additive]
theorem image_op_smul_distrib [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (f : F) (a : α) (s : Set α) :
    f '' (s <• a) = f '' s <• f a :=
  image_comm fun _ ↦ map_mul ..

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