instCoeConvexCone — Mathlib

English

There is a canonical embedding of pointed cones into convex cones, sending each pointed cone to its associated convex cone via a natural coercion.

Русский

Существует естественное вложение указанных конусов в выпуклые конусы, переводя каждый pointed cone в соответствующий ConvexCone через естественную вложенность.

LaTeX

$$$\\text{PointedCone}(R,E) \\hookrightarrow \\text{ConvexCone}(R,E),\\quad C \\mapsto C^{\\mathrm{toConvexCone}}$$$

Lean4

instance : Coe (PointedCone R E) (ConvexCone R E) where coe := toConvexCone

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