coe_toContinuousLinearEquiv_symm'

English

The symmetrical coercion from a linear equivalence’s continuous linear equivalence back to a linear equivalence is the symmetry of the original.

Русский

Симметрическое приведение обратно к линейной эквивалентности сохраняет симметрию исходного отображения.

LaTeX

$$@[simp] (e : E ≃ₗ[𝕜] F) : (e.toContinuousLinearEquiv.symm : F →ₗ[𝕜] E) = e.symm$$

Lean4

@[simp]
theorem coe_toContinuousLinearEquiv_symm' (e : E ≃ₗ[𝕜] F) : (e.toContinuousLinearEquiv.symm : F → E) = e.symm :=
  rfl

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