image_mul_left' — Mathlib

English

The map x → a x is a bijection; the image under this map of t equals the preimage under the corresponding inverse-left map.

Русский

Отображение x → a x биективно; образ под этим отображением множества t равен предобразу под соответствующим отображением левой инверсии.

LaTeX

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

Lean4

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

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