continuous_univBall — Mathlib

English

The map univBall(c,r) is continuous in its argument, hence a continuous deformation between the space and the ball.

Русский

Отображение univBall(c,r) непрерывно по аргументу, т.е. непрерывно деформирует пространство в шар.

LaTeX

$$$\text{Continuous}(\mathrm{univBall}(c,r)).$$$

Lean4

@[continuity]
theorem continuous_univBall (c : P) (r : ℝ) : Continuous (univBall c r) := by
  simpa [continuousOn_univ] using (univBall c r).continuousOn

Похожие утверждения