toConvexCone_inf

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.toConvexCone_inf

English

The convex cone associated to the bottom submodule is the zero cone.

Русский

Выпуклый конус, связанный с нулевым подмодулем, равен нулевому конусу.

LaTeX

$$bot^{\\text{toConvexCone}} = 0$$

Lean4

@[simp]
theorem toConvexCone_inf (C₁ C₂ : Submodule R M) : (C₁ ⊓ C₂).toConvexCone = C₁.toConvexCone ⊓ C₂.toConvexCone :=
  rfl

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

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

Разделы

Аффилиация

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