mem_intrinsicFrontier — Mathlib

English

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

Русский

Граница внутренности — это образ границы предобраза через аффинную аппроксимацию.

LaTeX

$$$$ x \in \operatorname{intrinsicFrontier}_{\kappa}(s) \iff \exists y \; y \in \operatorname{frontier}( \operatorname{preimage}(\operatorname{val}, s) ) \land \uparrow y = x. $$$$

Lean4

@[simp]
theorem mem_intrinsicFrontier :
    x ∈ intrinsicFrontier 𝕜 s ↔ ∃ y, y ∈ frontier ((↑) ⁻¹' s : Set <| affineSpan 𝕜 s) ∧ ↑y = x :=
  mem_image _ _ _

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