symm_equivOfInverse' — Mathlib

English

For the prime variant, the forward mapping of equivOfInverse' sends x to f1(x).

Русский

Для варианта с апострофом переход вперед у equivOfInverse' отправляет x в f1(x).

LaTeX

$$$(\\text{equivOfInverse'}(f_1,f_2,h_1,h_2))(x) = f_1(x)$$$

Lean4

/-- The inverse of `equivOfInverse'` is obtained by swapping the order of its parameters. -/
@[simp]
theorem symm_equivOfInverse' (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ h₁ h₂) :
    (equivOfInverse' f₁ f₂ h₁ h₂).symm = equivOfInverse' f₂ f₁ h₂ h₁ :=
  rfl

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