comap — Mathlib

English

If f is a linear map, the comap of a proper cone under f is again a proper cone in the domain space.

Русский

Для линейного отображения f разбор comap конуса образует новый правильный конус в исходном пространстве.

LaTeX

$$C.comap f ∈ ProperCone R E$$

Lean4

/-- The closure of image of a proper cone under a `R`-linear map is a proper cone. We
use continuous maps here so that the comap of f is also a map between proper cones. -/
abbrev comap (f : E →L[R] F) (C : ProperCone R F) : ProperCone R E :=
  ClosedSubmodule.comap (f.restrictScalars R≥0) C

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