equivOfInverse_apply — Mathlib

English

The inverse of the inverse construction is obtained by swapping the roles of f1 and f2; i.e., the inverse of equivOfInverse f1 f2 h1 h2 equals equivOfInverse f2 f1 h2 h1.

Русский

Обратное к той же самой конструкцие обратного отображения получается путём смены ролей f1 и f2; т. е. обратное к equivOfInverse f1 f2 h1 h2 равно equivOfInverse f2 f1 h2 h1.

LaTeX

$$$ (\\text{equivOfInverse}(f_1,f_2,h_1,h_2))^{-1} = \\text{equivOfInverse}(f_2,f_1,h_2,h_1) $$$

Lean4

@[simp]
theorem equivOfInverse_apply (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ h₁ h₂ x) : equivOfInverse f₁ f₂ h₁ h₂ x = f₁ x :=
  rfl

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