mem_toConvexCone

Mathlib.Geometry.Convex.Cone.Basic

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

English

For a submodule C, x ∈ C.toConvexCone if and only if x ∈ C.

Русский

Для подмодуля C верно: x принадлежит C.toConvexCone тогда и только тогда, когда x принадлежит C.

LaTeX

$$x \\in C^{\\text{toConvexCone}} \\iff x \\in C$$

Lean4

@[simp]
theorem mem_toConvexCone : x ∈ C.toConvexCone ↔ x ∈ C :=
  .rfl

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

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

Разделы

Аффилиация

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