closure_eq — Mathlib

English

Let K and L be convex cones in E. The closure of K as a cone equals L if and only if the closure of the underlying set of K (as a subset of E) equals L (as a subset of E).

Русский

Пусть K и L — выпуклые конусы в E. Замыкание K как конуса равно L тогда и только тогда, когда замыкание множества K как подмножества E равно L как подмножество E.

LaTeX

$$$K^{\text{closure}} = L \quad\iff\quad \operatorname{closure}(K \subseteq E) = L$$$

Lean4

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

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