Theorems · Theorem · group theory

vadd_preimage_set_subset

∀ {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) (c : M) (t : Set β), c +ᵥ ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (c +ᵥ t)

Defined in

Mathlib.GroupTheory.GroupAction.Pointwise

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

VAddVAddFunLikeAddActionHomClass