English
From a pointed convex cone, one constructs a pointed cone with the same carrier and compatible structure.
Русский
Из указанного выпуклого конуса берут pointed cone с тем же носителем и совместной структурой.
LaTeX
$$ConvexCone.toPointedCone (C) (hC) : PointedCone R E$$
Lean4
/-- The `PointedCone` constructed from a pointed `ConvexCone`. -/
def _root_.ConvexCone.toPointedCone (C : ConvexCone R E) (hC : C.Pointed) : PointedCone R E
where
carrier := C
add_mem' hx hy := C.add_mem hx hy
zero_mem' := hC
smul_mem' := fun ⟨c, hc⟩ x hx => by
simp_rw [SetLike.mem_coe]
rcases eq_or_lt_of_le hc with hzero | hpos
· unfold ConvexCone.Pointed at hC
convert hC
simp [← hzero]
· apply ConvexCone.smul_mem
· convert hpos
· exact hx
