mem_intrinsicInterior — Mathlib

English

The intrinsic interior maps x to an y on the interior preimage; x equals the image of y under the natural inclusion.

Русский

Внутренность отображает x как y внутри образа; x является образом y под естественным включением.

LaTeX

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

Lean4

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

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