English
The simp version asserts that equivOfInverse' acts on x by sending x to f1(x).
Русский
Упрощённая версия утверждает, что equivOfInverse' действует на x и отправляет x в f1(x).
LaTeX
$$$equivOfInverse' f_1 f_2 h_1 h_2 x = f_1(x)$$$
Lean4
/-- A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
continuous linear maps. See also `ContinuousLinearEquiv.arrowCongr`. -/
@[simps]
def arrowCongrEquiv (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) : (M₁ →SL[σ₁₄] M₄) ≃ (M₂ →SL[σ₂₃] M₃)
where
toFun f := (e₄₃ : M₄ →SL[σ₄₃] M₃).comp (f.comp (e₁₂.symm : M₂ →SL[σ₂₁] M₁))
invFun f := (e₄₃.symm : M₃ →SL[σ₃₄] M₄).comp (f.comp (e₁₂ : M₁ →SL[σ₁₂] M₂))
left_inv
f := ContinuousLinearMap.ext fun x => by simp only [ContinuousLinearMap.comp_apply, symm_apply_apply, coe_coe]
right_inv
f := ContinuousLinearMap.ext fun x => by simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]
