preimage_mul_left_one — Mathlib

English

If a map m is injective and its domain subsets s,t lie in the range of m, then preimage of the product equals product of preimages.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem preimage_mul_left_one : (a * ·) ⁻¹' 1 = {a⁻¹} := by rw [← image_mul_left', image_one, mul_one]

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