English
Under suitable hypotheses (nontrivial normed field, completeness, finite dimensionality, etc.), intrinsicClosure equals the ordinary topological closure.
Русский
При подходящих гипотезах (нетривиальное нормированное поле, полнота, конечномерность и т. д.) внутреннее замыкание совпадает с обычным топологическим замыканием.
LaTeX
$$intrinsicClosure_{\\mathbb{k}}(s) = closure(s)$$
Lean4
@[simp]
theorem image_intrinsicInterior (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) :
intrinsicInterior 𝕜 (φ '' s) = φ '' intrinsicInterior 𝕜 s :=
by
obtain rfl | hs := s.eq_empty_or_nonempty
· simp only [intrinsicInterior_empty, image_empty]
haveI : Nonempty s := hs.to_subtype
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
rw [intrinsicInterior, intrinsicInterior, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ←
Function.comp_assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm, ← preimage_comp,
Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp_id, preimage_comp,
φ.injective.preimage_image]
