intrinsicClosure_idem — Mathlib

English

IntrinsicClosure is idempotent: applying intrinsicClosure twice gives the same set.

Русский

IntrinsicClosure композиционно идемпотентно: применение дважды возвращает исходное множество.

LaTeX

$$intrinsicClosure_{\\mathbb{k}}(intrinsicClosure_{\\mathbb{k}}(s)) = intrinsicClosure_{\\mathbb{k}}(s)$$

Lean4

@[simp]
theorem intrinsicClosure_idem (s : Set P) : intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s :=
  by
  refine IsClosed.intrinsicClosure ?_
  set t := affineSpan 𝕜 (intrinsicClosure 𝕜 s) with ht
  clear_value t
  obtain rfl := ht.trans (affineSpan_intrinsicClosure _)
  rw [intrinsicClosure, preimage_image_eq _ Subtype.coe_injective]
  exact isClosed_closure

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