coe_map — Mathlib

English

The pointed cone of the image matches the closure of the mapped pointed cone.

Русский

Остроконечный конус образа совпадает с замкнутым образом направленного конуса.

LaTeX

$$C.map f).toPointedCone = PointedCone.map f.toLinearMap C.toPointedCone).closure$$

Lean4

@[simp, norm_cast]
theorem coe_map (f : E →L[R] F) (C : ProperCone R E) : C.map f = (C.toPointedCone.map (f : E →ₗ[R] F)).closure :=
  rfl

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