coe_toConvexCone

Mathlib.Geometry.Convex.Cone.Basic

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

English

The convex cone associated to a submodule C is exactly the same subset C of M.

Русский

Конус, связанный с подмодулем C, совпадает с самим подмодулем как подмножество M.

LaTeX

$$C^{\\text{toConvexCone}} = (C \\subseteq M)$$

Lean4

@[simp]
theorem coe_toConvexCone (C : Submodule R M) : C.toConvexCone = (C : Set M) :=
  rfl

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

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

Разделы

Аффилиация

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