continuous_skewAdjointPart

Mathlib.Topology.Algebra.Module.Star

URI: https://scilib.ai/kg/mathlib#continuous_skewAdjointPart

← MathLib Explorer

English

The skew-adjoint part map is continuous linear.

Русский

Отображение кососопряжённой части непрерывно линейно.

LaTeX

$$$\text{continuous}(\text{skewAdjointPart})$$$

Lean4

theorem continuous_skewAdjointPart [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] :
    Continuous (skewAdjointPart R (A := A)) :=
  ((continuous_const_smul _).comp <| continuous_id.sub continuous_star).subtype_mk _

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

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

Разделы

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

Аффилиация

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