image_mul_right — Mathlib

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

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