continuousOn_univBall_symm — Mathlib

English

The inverse of univBall is continuous on the ball centered at c with radius r.

Русский

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

LaTeX

$$$\text{ContinuousOn}(\mathrm{univBall}(c,r)^{-1})\; (\mathrm{ball}(c,r)).$$$

Lean4

theorem continuousOn_univBall_symm (c : P) (r : ℝ) : ContinuousOn (univBall c r).symm (ball c r) :=
  (univBall c r).symm.continuousOn.mono <| ball_subset_univBall_target c r

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