isClosed — Mathlib

English

If the ambient space is T2 (Hausdorff), then a compact convex body is closed; more generally, ConvexBody.isClosed asserts the underlying set is closed under the T2 assumption.

Русский

Пусть пространство — Хаусдорфово; компактное выпуклое множество замкнуто.

LaTeX

$$$\text{IsClosed}(K)$$$

Lean4

protected theorem isClosed [T2Space V] (K : ConvexBody V) : IsClosed (K : Set V) :=
  K.isCompact.isClosed

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