preimage_smul_setₛₗ — Mathlib

English

In a group context, for a group hom σ and a map f, f⁻¹'(σ c • t) = c • f⁻¹'(t) for a group element c.

Русский

В контексте группы, для гомоморфизма σ и отображения f, выполняется f⁻¹'(σ c • t) = c • f⁻¹'(t) для любого элемента c группы.

LaTeX

$$f^{-1}'(\sigma(c) \cdot t) = c \cdot f^{-1}'(t)$$

Lean4

/-- `preimage_smul_setₛₗ` in the context of groups -/
@[to_additive]
theorem preimage_smul_setₛₗ {G H α β : Type*} [Group G] [Group H] (σ : G → H) [MulAction G α] [MulAction H β]
    {F : Type*} [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β) :
    f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  preimage_smul_setₛₗ_of_isUnit_isUnit _ (Group.isUnit _) (Group.isUnit _) _

Похожие утверждения