intrinsicClosure — Mathlib

English

The intrinsic closure of s is the image in P of the topological closure of the preimage of s under the affine-span embedding.

Русский

Область собственного замыкания внутренности — образ в P замыкания по аффинному охватыванию.

LaTeX

$$$$ \operatorname{intrinsicClosure}_{\kappa}(s) = \operatorname{Im}\bigl( \operatorname{closure}(\operatorname{preimage}(\operatorname{val}, s)) \bigr). $$$$

Lean4

/-- The intrinsic closure of a set is its closure considered as a set in its affine span. -/
def intrinsicClosure (s : Set P) : Set P :=
  (↑) '' closure ((↑) ⁻¹' s : Set <| affineSpan 𝕜 s)

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