coe_toPointedCone — Mathlib

English

Membership in a pointed convex cone's corresponding pointed cone is equivalent to membership in the original convex cone.

Русский

Членство в точечном конусе выпуклого конуса соответствует членству в исходном конусе.

LaTeX

$$x ∈ C.toPointedCone hC ↔ x ∈ C$$

Lean4

@[simp, norm_cast]
theorem _root_.ConvexCone.coe_toPointedCone (C : ConvexCone R E) (hC : C.Pointed) : C.toPointedCone hC = C :=
  rfl

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