linearIsometryBoundedOfCompact_symm_apply

English

The inverse of the linear isometry bounded of compact α, E, 𝕜 sends a bounded continuous map f back to its corresponding continuous map, i.e., symm f = f.toContinuousMap.

Русский

Обратное отображение линейной изометрии, связанной с компактизмом, переводит ограниченное непрерывное отображение обратно в соответствующее непрерывное отображение: симм f = f.toContinuousMap.

LaTeX

$$$ (linearIsometryBoundedOfCompact \ α\ E\ 𝕜)^{\! -1} f = f^{\text{toContinuousMap}} $.$$

Lean4

@[simp]
theorem linearIsometryBoundedOfCompact_symm_apply (f : α →ᵇ E) :
    (linearIsometryBoundedOfCompact α E 𝕜).symm f = f.toContinuousMap :=
  rfl

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