toConvexCone_positive — Mathlib

English

The underlying set of the pointed cone positive matches the convex cone positive: ↑(positive R E) = ConvexCone.positive R E.

Русский

Множество, лежащее в основании направленного конуса positive, совпадает с положительным выпуклым конусом: ↑(positive R E) = ConvexCone.positive R E.

LaTeX

$$$\uparrow(\text{positive }R E) = \text{ConvexCone.positive }R E$$$

Lean4

@[simp, norm_cast]
theorem toConvexCone_positive : ↑(positive R E) = ConvexCone.positive R E :=
  rfl

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