affinity_unitBall — Mathlib

English

The map y ↦ x + y is an affine bijection sending the unit ball to the ball of radius r around x, provided r>0: x +ᵥ r • ball(0,1) = ball(x,r).

Русский

Аффинное отображение переносит единичный шар в шар радиуса r вокруг x: x +ᵥ r • B(0,1) = B(x,r).

LaTeX

$$$x +\\!_v (\\,r \\cdot B(0,1)\\,) = B(x,r)$$$

Lean4

/-- Any ball `Metric.ball x r`, `0 < r` is the image of the unit ball under `fun y ↦ x + r • y`. -/
theorem affinity_unitBall {r : ℝ} (hr : 0 < r) (x : E) : x +ᵥ r • ball (0 : E) 1 = ball x r := by
  rw [smul_unitBall_of_pos hr, vadd_ball_zero]

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