coe_mkOfIsCompactOperator — Mathlib

English

The constructed mkOfIsCompactOperator hf is a member of the space of compact operators.

Русский

Собранный объект mkOfIsCompactOperator hf является элементом множества компактных операторов.

LaTeX

$$$\\mathrm{mkOfIsCompactOperator}(hf) \\in \\mathrm{compactOperator}(\\sigma_{12}, M_1, M_2)$$$

Lean4

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

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