mathlib3 documentation

algebra.module.pointwise_pi

Pointwise actions on sets in Pi types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ι), has_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 : ι), has_vadd K (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 : ι), has_vadd K (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 : ι), has_smul K (R i)] (r : K) (t : Π (i : ι), set (R i)) :
theorem vadd_pi {K : Type u_1} {ι : Type u_2} {R : ι Type u_3} [add_group K] [Π (i : ι), add_action 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} [group K] [Π (i : ι), mul_action 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} [group_with_zero K] [Π (i : ι), mul_action K (R i)] {r : K} (S : set ι) (t : Π (i : ι), set (R i)) (hr : r 0) :
r S.pi t = S.pi (r t)