isClosed_intrinsicFrontier — Mathlib

English

If the affine span of s is closed, then intrinsicFrontier(s) is closed.

Русский

Если аффинное пространство, порожденное s, замкнуто, то intrinsicFrontier(s) замкнуто.

LaTeX

$$IsClosed(affineSpan_{\\mathbb{k}}(s)) \\Rightarrow IsClosed(intrinsicFrontier_{\\mathbb{k}}(s))$$

Lean4

theorem isClosed_intrinsicFrontier (hs : IsClosed (affineSpan 𝕜 s : Set P)) : IsClosed (intrinsicFrontier 𝕜 s) :=
  hs.isClosedEmbedding_subtypeVal.isClosedMap _ isClosed_frontier

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