smul_set_prod — Mathlib

English

Let M act on two types α and β. For any c in M and any sets S ⊆ α, T ⊆ β, the action distributes over the Cartesian product: c · (S × T) = (c · S) × (c · T).

Русский

Пусть M действует на множества α и β. Пусть c ∈ M и S ⊆ α, T ⊆ β. Тогда действие над декартовым произведением распределяется: c · (S × T) = (c · S) × (c · T).

LaTeX

$$$ c \cdot (S \times T) = (c \cdot S) \times (c \cdot T) $$$

Lean4

@[to_additive vadd_set_prod]
theorem smul_set_prod {M α : Type*} [SMul M α] [SMul M β] (c : M) (s : Set α) (t : Set β) :
    c • (s ×ˢ t) = (c • s) ×ˢ (c • t) :=
  prodMap_image_prod (c • ·) (c • ·) s t

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