preimage_smul_setₛₗ — Mathlib

English

In the MonoidHom context, for a monoid homomorphism σ, f, and c a unit, we have f⁻¹'(σ c • t) = c • f⁻¹'(t).

Русский

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

LaTeX

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

Lean4

/-- `preimage_smul_setₛₗ` when `c` is a unit and `σ` is a monoid homomorphism. -/
@[to_additive]
protected theorem preimage_smul_setₛₗ {F : Type*} (σ : M →* N) [FunLike F α β] [MulActionSemiHomClass F σ α β] (f : F)
    (hc : IsUnit c) (t : Set β) : f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  hc.preimage_smul_setₛₗ σ f t

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