equivOfInverse'_apply — Mathlib

English

Applying the constructed equivalence equivOfInverse to an input x ∈ M1 yields f1(x).

Русский

При применение сконструированного эквивелента equivOfInverse к элементу x ∈ M1 получаем f1(x).

LaTeX

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

Lean4

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

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