instBot

Mathlib.Geometry.Convex.Cone.Basic

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

English

The bottom element of ConvexCone R M is the empty set; it contains no vectors.

Русский

Нижний элемент множества выпуклых конусов ConvexCone R M равен пустому множеству; он не содержит векторов.

LaTeX

$$⊥_{ConvexCone(R,M)} = ∅$$

Lean4

instance : Bot (ConvexCone R M) :=
  ⟨⟨∅, fun _ _ _ => False.elim, fun _ => False.elim⟩⟩

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

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

Разделы

Аффилиация

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