image_mul_left — Mathlib

English

For every a in a group, the map x → a x is a bijection. Consequently, the image of a Finset t under this map equals the preimage of t under the inverse-left map, i.e. image (b → a b) t = preimage t (b → a^{-1} b).

Русский

Для любого a в группе отображение x → a x является биекцией. Следовательно, образ конечного множества t под этим отображением равен обратному образу t под отображением b → a^{-1} b.

LaTeX

$$$\operatorname{image}(b \mapsto a b)(t) = \operatorname{preimage}(t)(b \mapsto a^{-1} b)$$$

Lean4

@[to_additive (attr := simp)]
theorem image_mul_left : image (fun b => a * b) t = preimage t (fun b => a⁻¹ * b) (mul_right_injective _).injOn :=
  coe_injective <| by simp

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