instAddZeroClass

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.instAddZeroClass

English

Simplified membership: x ∈ C1 + C2 iff ∃ y ∈ C1, ∃ z ∈ C2, y + z = x.

Русский

Упрощённое членство: x ∈ C1 + C2 тогда и только тогда, когда существует y ∈ C1, z ∈ C2, такое что y+z = x.

LaTeX

$$x ∈ C_1 + C_2 \iff ∃ y ∈ C_1, ∃ z ∈ C_2, y + z = x$$

Lean4

instance instAddZeroClass : AddZeroClass (ConvexCone R M)
    where
  zero_add _ := by ext; simp
  add_zero _ := by ext; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru