isClosed_intrinsicClosure — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isClosed_intrinsicClosure (hs : IsClosed (affineSpan 𝕜 s : Set P)) : IsClosed (intrinsicClosure 𝕜 s) :=
  hs.isClosedEmbedding_subtypeVal.isClosedMap _ isClosed_closure

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