smul_set_pi — Mathlib

English

Let G act on each α_i (i in I). For any c ∈ G, the product of subsets s_i ⊆ α_i is compatible with the action: c · ∏_{i∈I} s_i = ∏_{i∈I} (c · s_i).

Русский

Пусть G действует на каждое множество α_i (для i в I). Для любого c ∈ G произведение подмножеств s_i ⊆ α_i согласуется с действием: c · ∏_{i∈I} s_i = ∏_{i∈I} (c · s_i).

LaTeX

$$$ c \cdot \Big( \prod_{i \in I} s_i \Big) = \prod_{i \in I} (c \cdot s_i) $$$

Lean4

@[to_additive]
theorem smul_set_pi {G ι : Type*} {α : ι → Type*} [Group G] [∀ i, MulAction G (α i)] (c : G) (I : Set ι)
    (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s) :=
  smul_set_pi_of_surjective c I s fun _ _ ↦ (MulAction.bijective c).surjective

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