preimage_mul — Mathlib

English

If m is injective and range conditions hold, the preimage of a product equals the product of preimages.

Русский

Если m инъективно и соблюдаются условия на образ, то предобраз произведения равен произведению предобразов.

LaTeX

$$$ m^{-1}' (s * t) = m^{-1}' s * m^{-1}' t $$$

Lean4

@[to_additive]
theorem preimage_mul (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) :
    m ⁻¹' (s * t) = m ⁻¹' s * m ⁻¹' t :=
  hm.image_injective <| by
    rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

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