instAddMemClass

Mathlib.Geometry.Convex.Cone.Basic

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

English

The convex cone structure supports an additive membership class.

Русский

Структура конуса допускает членство в сложении как класс.

LaTeX

$$AddMemClass (ConvexCone R M) M$$

Lean4

instance : AddMemClass (ConvexCone R M) M where add_mem ha hb := add_mem' _ ha hb

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

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

Разделы

Аффилиация

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