English
If s is a convex bounded set with nonempty interior, there exists a homeomorphism sending interior s to the unit open ball and closure s to the unit closed ball, and frontier to the unit sphere.
Русский
При выпуклом ограниченном множество s с ненулимой interior существует гомеоморфизм, переводящий interior s в единичный открытый шар, closure s в единичный замкнутый шар и frontier в единичную сферу.
LaTeX
$$$\\exists h : E \\to E,\\; h'' interior s = ball(0,1) \\wedge h'' closure s = closedBall(0,1) \\wedge h'' frontier s = sphere(0,1)$$$
Lean4
/-- If `s` is a convex bounded set with a nonempty interior in a real normed space,
then there is a homeomorphism of the ambient space to itself
that sends the interior of `s` to the unit open ball
and the closure of `s` to the unit closed ball. -/
theorem exists_homeomorph_image_interior_closure_frontier_eq_unitBall {s : Set E} (hc : Convex ℝ s)
(hne : (interior s).Nonempty) (hb : IsBounded s) :
∃ h : E ≃ₜ E, h '' interior s = ball 0 1 ∧ h '' closure s = closedBall 0 1 ∧ h '' frontier s = sphere 0 1 := by
simpa [isOpen_ball.interior_eq, closure_ball, frontier_ball] using
exists_homeomorph_image_eq hc hne (NormedSpace.isVonNBounded_of_isBounded _ hb) (convex_ball 0 1)
(by simp [isOpen_ball.interior_eq]) (NormedSpace.isVonNBounded_ball _ _ _)
