toConvexCone_top

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.toConvexCone_top

English

The convex cone associated to the top submodule is the top convex cone.

Русский

Выпуклый конус, связанный с вершиной подмодуля, равен верхнему выпуклому конусу.

LaTeX

$$top^{\\text{toConvexCone}} = \\text{top convex cone}$$

Lean4

@[simp]
theorem toConvexCone_top : (⊤ : Submodule R M).toConvexCone = ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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