instZero

Mathlib.Geometry.Convex.Cone.Pointed

URI: https://scilib.ai/kg/mathlib#PointedCone.instZero

English

Every pointed cone contains the zero vector; the zero of the cone is the pair (0, proof).

Русский

Любой pointed cone содержит нулевой вектор; ноль конуса задаётся как пара (0, доказательство).

LaTeX

$$Zero C$$

Lean4

instance instZero (C : PointedCone R E) : Zero C :=
  ⟨0, C.zero_mem⟩

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

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

Разделы

Аффилиация

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