inv_range — Mathlib

English

The inverse of the image of a function equals the image of the inverse function at the level of elements.

Русский

Обратное образа функции равняется образу обратной функции на уровне элементов.

LaTeX

$$$ (\operatorname{range} f)^{-1} = \operatorname{range} (i \mapsto f(i)^{-1}) $$$

Lean4

@[to_additive]
theorem inv_range {ι : Sort*} {f : ι → α} : (range f)⁻¹ = range fun i => (f i)⁻¹ :=
  by
  rw [← image_inv_eq_inv]
  exact (range_comp ..).symm

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