linearIsometryBoundedOfCompact_toAddEquiv

English

The linearIsometryBoundedOfCompact_toAddEquiv lemma states that the underlying linear isomorphism corresponds to addEquivBoundedOfCompact.

Русский

Лемма показывает, что соответствие линейной изометрии эквивалентно addEquivBoundedOfCompact.

LaTeX

$$$ (linearIsometryBoundedOfCompact \alpha \ E \ 𝕜).toLinearEquiv.toAddEquiv = addEquivBoundedOfCompact \alpha \ E $.$$

Lean4

@[simp]
theorem linearIsometryBoundedOfCompact_toAddEquiv :
    ((linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv : C(α, E) ≃+ (α →ᵇ E)) = addEquivBoundedOfCompact α E :=
  rfl

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