pointed_toConvexCone

Mathlib.Geometry.Convex.Cone.Pointed

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

English

If C is a pointed cone, then its associated convex cone is pointed as well.

Русский

Пусть C — pointed cone; соответствующий выпуклый конус также имеет свойство pointed.

LaTeX

$$(C : ConvexCone R E).Pointed$$

Lean4

@[simp]
theorem pointed_toConvexCone (C : PointedCone R E) : (C : ConvexCone R E).Pointed := by
  simp [toConvexCone, ConvexCone.Pointed]

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

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

Разделы

Аффилиация

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