map_inv — Mathlib

English

Let f: α → β. The induced map commutes with taking inverses: f̂(x^{-1}) = (f̂(x))^{-1} for all x in FreeGroup(α).

Русский

Пусть f: α → β. Приведённое отображение сохраняет операцию взятия обратного: f̂( x^{-1} ) = (f̂(x))^{-1} для любого x в FreeGroup(α).

LaTeX

$$$$\\forall f:\\alpha \\to \\beta,\\ \\forall x\\in \\mathrm{FreeGroup}(\\alpha),\\ \\widehat{f}(x^{-1})=\\widehat{f}(x)^{-1}.$$$$

Lean4

@[to_additive (attr := simp)]
theorem map_inv (f : α → β) (x : FreeGroup α) : f <$> x⁻¹ = (f <$> x)⁻¹ :=
  (map f).map_inv x

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