preimage_smul_set — Mathlib

English

In a general setting with IsUnit, for any f and t, f ⁻¹' (c • t) = c • f ⁻¹' t holds when c is a unit and σ is a monoid action.

Русский

В общем случае с IsUnit: для любого f и t выполняется f⁻¹'(c • t) = c • f⁻¹'(t) при c — единица и σ — гомоморфизм.

LaTeX

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

Lean4

@[to_additive]
theorem preimage_smul_set {G : Type*} [Group G] {α β : Type*} [MulAction G α] [MulAction G β] {F : Type*}
    [FunLike F α β] [MulActionHomClass F G α β] (f : F) (c : G) (t : Set β) : f ⁻¹' (c • t) = c • f ⁻¹' t :=
  (Group.isUnit c).preimage_smul_set f t

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