map_id

Mathlib.Analysis.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ProperCone.map_id

English

The map of a cone under f can be described via closure of the pointed cone image.

Русский

Образ конуса через отображение f описывается через замкнутость изображения направленного конуса.

LaTeX

$$C.map f = (C.toPointedCone.map f.toLinearMap).closure$$

Lean4

@[simp]
theorem map_id (C : ProperCone R F) : C.map (.id _ _) = C :=
  ClosedSubmodule.map_id _

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

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

Разделы

Аффилиация

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