extend_inv — Mathlib

English

If γ has an inverse operation, then extending f with g^{-1} and e^{-1} yields the inverse of the extension: extend f g^{-1} e^{-1} = (extend f g e)^{-1}.

Русский

Если γ имеет операцию взятия обратного, то расширение f по g^{-1} и e^{-1} равно обратному расширению: extend f g^{-1} e^{-1} = (extend f g e)^{-1}.

LaTeX

$$$ \mathrm{extend} f g^{-1} e^{-1} = (\mathrm{extend} f g e)^{-1} $$$

Lean4

@[to_additive]
theorem extend_inv [Inv γ] (f : α → β) (g : α → γ) (e : β → γ) :
    Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹ := by
  classical
  funext x
  simp [Function.extend_def, apply_dite Inv.inv]

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