preimage_smul_setₛₗ — Mathlib

English

For monoid actions, if c is a unit, then f⁻¹'(σ c • t) = c • f⁻¹'(t).

Русский

Для действий моноида, если 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]
theorem preimage_smul_setₛₗ {F G : Type*} [FunLike G M N] [MonoidHomClass G M N] (σ : G) [FunLike F α β]
    [MulActionSemiHomClass F σ α β] (f : F) (hc : IsUnit c) (t : Set β) : f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  preimage_smul_setₛₗ_of_isUnit_isUnit _ hc (hc.map _)
    _
      -- TODO: when you remove the next 2 aliases,
      -- please move the group version below out of the `Group` namespace.

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