coe_closure

Mathlib.Analysis.Convex.Cone.Closure

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

English

The coercion-closure of a convex cone expresses closure of the cone's image.

Русский

Замыкание через отображение конуса выражает замыкание образа конуса.

LaTeX

$$coe_closure (K) = closure (coe K)$$

Lean4

@[simp, norm_cast]
theorem coe_closure (K : ConvexCone 𝕜 E) : (K.closure : Set E) = closure K :=
  rfl

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

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

Разделы

Аффилиация

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