toPointedCone_top

Mathlib.Geometry.Convex.Cone.Pointed

URI: https://scilib.ai/kg/mathlib#ConvexCone.toPointedCone_top

English

The top element of convex cones, when transformed to pointed cones via toPointedCone, yields the top pointed cone.

Русский

Верхний элемент выпуклых конусов переходит в верхний pointed cone через toPointedCone.

LaTeX

$$ConvexCone.toPointedCone_top$$

Lean4

@[simp]
theorem _root_.ConvexCone.toPointedCone_top : (⊤ : ConvexCone R E).toPointedCone trivial = ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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