smulTorsor_preimage_ball — Mathlib

English

For hk ≠ 0, the preimage of the ball of radius ||k|| around c under the dilation smulTorsor lies precisely in the unit ball around 0 in E.

Русский

При hk ≠ 0 предобраз шара радиусом ||k|| вокруг c по дилатации smulTorsor совпадает с единичным шаром вокруг 0 в E.

LaTeX

$$$$\smulTorsor(c, hk)^{-1}(\mathrm{Ball}(c, \|k\|)) = \mathrm{Ball}(0, 1).$$$$

Lean4

@[simp]
theorem smulTorsor_preimage_ball {c : P} {k : 𝕜} (hk : k ≠ 0) :
    smulTorsor c hk ⁻¹' (Metric.ball c ‖k‖) = Metric.ball (0 : E) 1 := by aesop (add simp norm_smul)

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