map — Mathlib

English

The image of a pointed cone under a linear map corresponds to the image of the associated convex cone under the same map.

Русский

Образ конуса в выпуклом конусе соответствует образу соответствующего конуса под тем же отображением.

LaTeX

$$PointedCone.map f C$$

Lean4

/-- The image of a pointed cone under an `R`-linear map is a pointed cone. -/
def map (f : E →ₗ[R] F) (C : PointedCone R E) : PointedCone R F :=
  Submodule.map (f : E →ₗ[R≥0] F) C

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