English
For any center c and radius r, the map univBall(c,r) is given by a smooth affine construction when r>0, and by a translation by c when r≤0.
Русский
Для любого центра c и радиуса r отображение univBall(c,r) определяется как гладко-афинное отображение при r>0, иначе — как сдвиг на вектор c.
LaTeX
$$$\text{Если } r>0,\ univBall(c,r) = \text{univUnitBall} \;{\trans} \big(\text{unitBallBall}(c,r,h)\big) ;\text{ иначе } univBall(c,r) = (x \mapsto x+c).$$$
Lean4
/-- If `r > 0`, then `OpenPartialHomeomorph.univBall c r` is a smooth open partial homeomorphism
with `source = Set.univ` and `target = Metric.ball c r`.
Otherwise, it is the translation by `c`.
Thus in all cases, it sends `0` to `c`, see `OpenPartialHomeomorph.univBall_apply_zero`. -/
def univBall (c : P) (r : ℝ) : OpenPartialHomeomorph E P :=
if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) rfl
else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph
