intrinsicClosure_eq_closure_inter_affineSpan

English

The intrinsic closure of s is the intersection of its topological closure with its affine span.

Русский

Внутреннее замыкание множества равно пересечению его замыкания в топологии и образующего пространства.

LaTeX

$$intrinsicClosure_{\\mathbb{k}}(s) = closure(s) \\cap affineSpan_{\\mathbb{k}}(s)$$

Lean4

theorem intrinsicClosure_eq_closure_inter_affineSpan (s : Set P) : intrinsicClosure 𝕜 s = closure s ∩ affineSpan 𝕜 s :=
  by
  have h : Topology.IsInducing ((↑) : affineSpan 𝕜 s → P) := .subtypeVal
  rw [intrinsicClosure, h.closure_eq_preimage_closure_image, Set.image_preimage_eq_inter_range,
    Set.image_preimage_eq_of_subset ?_, Subtype.range_coe]
  rw [Subtype.range_coe]
  apply subset_affineSpan

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