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