mem_intrinsicClosure — Mathlib

English

The intrinsic frontier of s is contained in the intrinsic closure of s.

Русский

Граница внутренности содержится в внутреннем замыкании s.

LaTeX

$$$$ \\operatorname{intrinsicFrontier}_{\\kappa}(s) \\subseteq \\operatorname{intrinsicClosure}_{\\kappa}(s). $$$$

Lean4

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

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