intrinsicClosure_singleton — Mathlib

English

The intrinsic closure of a singleton is the singleton itself.

Русский

Внутреннее замыкание множества‑одиночки равно самой одиночке.

LaTeX

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

Lean4

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

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