English
There is an affine homeomorphism between the unit ball and an arbitrary ball: the map x ↦ c + r x with r > 0 carries ball(0,1) onto ball(c,r).
Русский
Существует афинное гомеоморфизм между единичным шаром и произвольным шаром: отображение x ↦ c + r x с r > 0 переводит ball(0,1) в ball(c,r).
LaTeX
$$$\exists c \in P, r>0:\ h: E \to P,\ h(x)=c+r x,\ h\text{ переводит }\mathrm{ball}(0,1) \text{ onto } \mathrm{ball}(c,r).$$$
Lean4
/-- Affine homeomorphism `(r • · +ᵥ c)` between a normed space and an add torsor over this space,
interpreted as an `OpenPartialHomeomorph` between `Metric.ball 0 1` and `Metric.ball c r`. -/
@[simps!]
def unitBallBall (c : P) (r : ℝ) (hr : 0 < r) : OpenPartialHomeomorph E P :=
((Homeomorph.smulOfNeZero r hr.ne').trans (IsometryEquiv.vaddConst c).toHomeomorph).toOpenPartialHomeomorphOfImageEq
(ball 0 1) isOpen_ball (ball c r) <|
by
change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r
rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
simp [abs_of_pos hr]
