English
The sum of two convex cones C1 and C2 is again a convex cone.
Русский
Сумма двух выпуклых конусов C1 и C2 снова является выпуклым конусом.
LaTeX
$$C_1 + C_2 ∈ ConvexCone(R,M)$$
Lean4
instance instAdd : Add (ConvexCone R M) where
add C₁
C₂ :=
{ carrier := C₁ + C₂
smul_mem' := by
rintro c hc _ ⟨x, hx, y, hy, rfl⟩
rw [smul_add]
use c • x, C₁.smul_mem hc hx, c • y, C₂.smul_mem hc hy
add_mem' := by
rintro _ ⟨x₁, hx₁, x₂, hx₂, rfl⟩ y ⟨y₁, hy₁, y₂, hy₂, rfl⟩
exact ⟨x₁ + y₁, add_mem hx₁ hy₁, x₂ + y₂, add_mem hx₂ hy₂, add_add_add_comm ..⟩ }