preimage_smul_set — Mathlib

English

Under IsUnit for c and σ c, the preimage-smul equality holds: f ⁻¹' (σ c • t) = c • f ⁻¹' t.

Русский

При единице c и σ c выполняется равенство предобразного умножения: f⁻¹'(σ c • t) = c • f⁻¹'(t).

LaTeX

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

Lean4

@[to_additive]
theorem preimage_smul_set {M α β F : Type*} [Monoid M] [MulAction M α] [MulAction M β] [FunLike F α β]
    [MulActionHomClass F M α β] (f : F) {c : M} (hc : IsUnit c) (t : Set β) : f ⁻¹' (c • t) = c • f ⁻¹' t :=
  preimage_smul_setₛₗ_of_isUnit_isUnit f hc hc t

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