intrinsicFrontier — Mathlib

English

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

Русский

Граница внутренности множества s — это образ в P границы preimage(s) в аффинном охватывании.

LaTeX

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

Lean4

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

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