English
The symmetry-inverse map of univBall is continuous on the ball when appropriate.
Русский
Обратное отображение симметрии univBall непрерывно на шаре при надлежащих условиях.
LaTeX
$$$\text{ContinuousOn}(\mathrm{univBall}(c,r)^{-1}) (\mathrm{ball}(c,r)).$$$
Lean4
theorem infEdist_smul₀ {c : 𝕜} (hc : c ≠ 0) (s : Set E) (x : E) :
EMetric.infEdist (c • x) (c • s) = ‖c‖₊ • EMetric.infEdist x s :=
by
simp_rw [EMetric.infEdist]
have : Function.Surjective ((c • ·) : E → E) := Function.RightInverse.surjective (smul_inv_smul₀ hc)
trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
· refine (this.iInf_congr _ fun y => ?_).symm
simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀]
· have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]
