instAdd — Mathlib

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 ..⟩ }

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