starₗᵢ_apply

Mathlib.Analysis.CStarAlgebra.Basic

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

English

The star linear isomorphism corresponds to the continuous linear equivalence starL 𝕜.

Русский

Линейное изоморфизм звезды эквивалентен непрерывному линейному эквиваленту starL 𝕜.

LaTeX

$$$ (star\_\ell^{\;\mathbb{K}}).toContinuousLinearEquiv = (starL\ 𝕜) $$$

Lean4

theorem starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x :=
  rfl

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

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

Разделы

Аффилиация

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