comap

Mathlib.Geometry.Convex.Cone.Pointed

URI: https://scilib.ai/kg/mathlib#PointedCone.comap

← MathLib Explorer

English

The preimage of a pointed cone under a linear map is again a pointed cone.

Русский

Образ предобраза под линейным отображением является снова pointed cone.

LaTeX

$$def comap (f) (C) : PointedCone R E$$

Lean4

/-- The preimage of a pointed cone under an `R`-linear map is a pointed cone. -/
def comap (f : E →ₗ[R] F) (C : PointedCone R F) : PointedCone R E :=
  Submodule.comap (f : E →ₗ[R≥0] F) C

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

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

Разделы

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

Аффилиация

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