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)

source

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)

source

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)) :

r +ᵥ set.univ.pi t = set.univ.pi (r +ᵥ t)

source

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)) :

r • set.univ.pi t = set.univ.pi (r • t)

source

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)

source

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)

source

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)