intrinsicInterior_singleton — Mathlib

English

The intrinsic interior of a singleton equals the singleton itself.

Русский

Внутренность множества‑одиночки равна самому этому элементу.

LaTeX

$$$\\operatorname{intrinsicInterior}_{\\mathbb{k}}(\\{x\\}) = \\{x\\}$$$

Lean4

@[simp]
theorem intrinsicInterior_singleton (x : P) : intrinsicInterior 𝕜 ({ x } : Set P) = { x } := by
  simp only [intrinsicInterior, preimage_coe_affineSpan_singleton, interior_univ, image_univ, Subtype.range_coe_subtype,
    mem_affineSpan_singleton, setOf_eq_eq_singleton]

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