English
If f1: M1 →SL[σ₁₂] M2 and f2: M2 →SL[σ₂₁] M1 satisfy left-inverse and right-inverse conditions, then there is a ContinuousLinearEquiv between M1 and M2 whose forward map is f1 and inverse is f2.
Русский
Если f1: M1 →SL[σ₁₂] M2 и f2: M2 →SL[σ₂₁] M1 удовлетворяют условиям левого и правого обращения, то существует непрерывно-линейное эквивАЛЕНтное отображение между M1 и M2, у которого переход вперед — f1, а обратное — f2.
LaTeX
$$$\\exists e : M_1 \\simeq_{σ_{12}} M_2 \\;\\text{defin ed by } e := \\text{equivOfInverse}(f_1,f_2,h_1,h_2),$$$
Lean4
/-- Create a `ContinuousLinearEquiv` from two `ContinuousLinearMap`s that are
inverse of each other. See also `equivOfInverse'`. -/
def equivOfInverse (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h₁ : Function.LeftInverse f₂ f₁)
(h₂ : Function.RightInverse f₂ f₁) : M₁ ≃SL[σ₁₂] M₂ :=
{ f₁ with
continuous_toFun := f₁.continuous
invFun := f₂
continuous_invFun := f₂.continuous
left_inv := h₁
right_inv := h₂ }
