preimage_smul_setₛₗ_of_isUnit_isUnit

English

When c is a unit and σ c is a unit, the smul-set 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

/-- `preimage_smul_setₛₗ` when both scalars act by unit -/
@[to_additive]
theorem preimage_smul_setₛₗ_of_isUnit_isUnit (f : F) (hc : IsUnit c) (hc' : IsUnit (σ c)) (t : Set β) :
    f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
  preimage_smul_setₛₗ' hc.smul_bijective.surjective hc'.smul_bijective.injective

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