mkOfIsCompactOperator_to_linearMap

English

The underlying map of mkOfIsCompactOperator hf is the original f.

Русский

Пусть hf задаёт компактный оператор f; тогда подлежащая линейная карта mkOfIsCompactOperator hf совпадает с f.

LaTeX

$$$(\\mathrm{mkOfIsCompactOperator}(hf) : M_1 \\to M_2) = f$$$

Lean4

@[simp]
theorem mkOfIsCompactOperator_to_linearMap {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) :
    (ContinuousLinearMap.mkOfIsCompactOperator hf : M₁ →ₛₗ[σ₁₂] M₂) = f :=
  rfl

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