starₗᵢ_toContinuousLinearEquiv

Mathlib.Analysis.CStarAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#starₗᵢ_toContinuousLinearEquiv

← MathLib Explorer

English

For any x ∈ E, starₗᵢ 𝕜 x = star x.

Русский

Для любого x ∈ E, starₗᵢ 𝕜 x = star x.

LaTeX

$$$ star\_\ell^{\;\mathbb{K}}\;x = \mathrm{star}(x) $$$

Lean4

@[simp]
theorem starₗᵢ_toContinuousLinearEquiv : (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = (starL 𝕜 : E ≃L⋆[𝕜] E) :=
  ContinuousLinearEquiv.ext rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru