toPointedCone — Mathlib

English

The coercion from ProperCone to PointedCone is injective; i.e., two proper cones having the same underlying set are equal.

Русский

Вложение из ProperCone в PointedCone инъективно; два конуса с одинаковым основанием равны.

LaTeX

$$Injective ((↑) : ProperCone(R,E) → PointedCone(R,E))$$

Lean4

/-- Any proper cone can be seen as a pointed cone.

This is an alias of `ClosedSubmodule.toSubmodule` for convenience and discoverability. -/
@[coe]
abbrev toPointedCone (C : ProperCone R E) : PointedCone R E :=
  C.toSubmodule

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