intrinsicClosure — Mathlib

English

If a subset s of a real vector space is convex, then its intrinsic closure is also convex.

Русский

Если множество s в вещественном векторном пространстве выпукло, то его внутренняя замкнутая оболочка тоже выпукла.

LaTeX

$$$ \operatorname{Convex}_{\mathbb{K}}(s) \Rightarrow \operatorname{Convex}_{\mathbb{K}}(\operatorname{intrinsicClosure}_{\mathbb{K}}(s)) $$$

Lean4

protected theorem intrinsicClosure (hs : Convex 𝕜 s) : Convex 𝕜 (intrinsicClosure 𝕜 s) :=
  by
  rw [intrinsicClosure_eq_closure_inter_affineSpan]
  exact hs.closure.inter (affineSpan 𝕜 s).convex

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