toConvexCone_map — Mathlib

English

There is a lifting structure linking convex cones with pointed cones via a canonical coercion.

Русский

Существует связь переноса структур между выпуклыми конусами и pointed конусами через каноническое отображение.

LaTeX

$$CanLift (ConvexCone R E) (PointedCone R E) (↑) ConvexCone.Pointed$$

Lean4

@[simp, norm_cast]
theorem toConvexCone_map (C : PointedCone R E) (f : E →ₗ[R] F) :
    (C.map f : ConvexCone R F) = (C : ConvexCone R E).map f :=
  rfl

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