# mathlibdocumentation

algebra.module.pointwise_pi

# Pointwise actions on sets in Pi types #

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

## Tags #

theorem smul_pi_subset {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [Π (i : ι), (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 : ι), (R i)] (r : K) (s : set ι) (t : Π (i : ι), set (R i)) :
r +ᵥ s.pi t s.pi (r +ᵥ t)
theorem vadd_univ_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [Π (i : ι), (R i)] (r : K) (t : Π (i : ι), set (R i)) :
theorem smul_univ_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [Π (i : ι), (R i)] (r : K) (t : Π (i : ι), set (R i)) :
r = set.univ.pi (r t)
theorem vadd_pi {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [add_group K] [Π (i : ι), (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} [group K] [Π (i : ι), (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} [Π (i : ι), (R i)] {r : K} (S : set ι) (t : Π (i : ι), set (R i)) (hr : r 0) :
r S.pi t = S.pi (r t)