English
For every b in a group, the map x → x b is a bijection. Hence image (x → x b) t equals preimage (under x → x b^{-1}) of t.
Русский
Для любого b в группе отображение x → x b является биекцией. Следовательно, образ t под x → x b равен предобразу t под обратному отображению.
LaTeX
$$$\operatorname{image}(x \mapsto x b)(t) = \operatorname{preimage}(t)(x \mapsto x b^{-1})$$$
Lean4
@[to_additive (attr := simp)]
theorem image_mul_right : image (· * b) t = preimage t (· * b⁻¹) (mul_left_injective _).injOn :=
coe_injective <| by simp