Theorems · Theorem · group theory

Set.MapsTo.vadd_set

∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β]
  [inst_2 : FunLike F α β] [AddActionHomClass F M α β] {f : F} {s : Set α} {t : Set β},
  Set.MapsTo (⇑f) s t → ∀ (c : M), Set.MapsTo (⇑f) (c +ᵥ s) (c +ᵥ t)

Defined in

Mathlib.GroupTheory.GroupAction.Pointwise

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

VAddVAddFunLikeAddActionHomClass