preimage_mul_preimage_subset — Mathlib

English

For sets s,t, the product of their preimages under m is contained in the preimage of the product s * t.

Русский

Произведение предобразов множеств s, t под м помещено в предобраз множества s * t.

LaTeX

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

Lean4

@[to_additive]
theorem preimage_mul_preimage_subset {s t : Set β} : m ⁻¹' s * m ⁻¹' t ⊆ m ⁻¹' (s * t) :=
  by
  rintro _ ⟨_, _, _, _, rfl⟩
  exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

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