English
Affine isometries preserve intrinsic frontier: the image of intrinsicFrontier is the intrinsicFrontier of the image.
Русский
Аффинные изометрии сохраняют внутpеннюю границу: образ intrinsicFrontier равен intrinsicFrontier образа.
LaTeX
$$intrinsicFrontier_{\\mathbb{k}}(φ''s) = φ'' intrinsicFrontier_{\\mathbb{k}}(s)$$
Lean4
@[simp]
theorem image_intrinsicClosure (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : intrinsicClosure 𝕜 (φ '' s) = φ '' intrinsicClosure 𝕜 s :=
by
obtain rfl | hs := s.eq_empty_or_nonempty
· simp
haveI : Nonempty s := hs.to_subtype
let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph
have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply
rw [intrinsicClosure, intrinsicClosure, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, ←
Function.comp_assoc, image_comp, image_comp, f.symm.image_closure, f.image_symm, ← preimage_comp,
Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp_id, preimage_comp,
φ.injective.preimage_image]
