Pointwise actions on sets in Pi types

This file contains lemmas about pointwise actions on sets in Pi types.

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication, pi

theorem smul_pi_subset {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → SMul K (R i)] (r : K) (s : Set ι) (t : (i : ι) → Set (R i)) : r • s.pi t ⊆ s.pi (r • t)

theorem vadd_pi_subset {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → VAdd K (R i)] (r : K) (s : Set ι) (t : (i : ι) → Set (R i)) : r +ᵥ s.pi t ⊆ s.pi (r +ᵥ t)

theorem smul_univ_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → SMul K (R i)] (r : K) (t : (i : ι) → Set (R i)) : r • Set.univ.pi t = Set.univ.pi (r • t)

theorem vadd_univ_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → VAdd K (R i)] (r : K) (t : (i : ι) → Set (R i)) : r +ᵥ Set.univ.pi t = Set.univ.pi (r +ᵥ t)

theorem smul_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [Group K] [(i : ι) → MulAction K (R i)] (r : K) (S : Set ι) (t : (i : ι) → Set (R i)) : r • S.pi t = S.pi (r • t)

theorem vadd_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [AddGroup K] [(i : ι) → AddAction K (R i)] (r : K) (S : Set ι) (t : (i : ι) → Set (R i)) : r +ᵥ S.pi t = S.pi (r +ᵥ t)

theorem smul_pi₀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [GroupWithZero K] [(i : ι) → MulAction K (R i)] {r : K} (S : Set ι) (t : (i : ι) → Set (R i)) (hr : r ≠ 0) : r • S.pi t = S.pi (r • t)