closure_eq

Mathlib.Analysis.Convex.Cone.Closure

URI: https://scilib.ai/kg/mathlib#PointedCone.closure_eq

English

For pointed cones K,L, K.closure = L iff closure(K:Set E) = L (as a set).

Русский

Для указательных конусов K и L, K.closure = L тогда и только тогда, когда closure(K:Set E) = L (как множество).

LaTeX

$$$K.closure = L \iff closure (K : Set E) = L$$$

Lean4

@[simp]
theorem closure_eq {K L : PointedCone 𝕜 E} : K.closure = L ↔ closure (K : Set E) = L :=
  SetLike.ext'_iff

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

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

Разделы

Аффилиация

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