smul_ball_preimage — Mathlib

English

A ball around some center absorbs a smaller ball around the same center.

Русский

Шар вокруг некоторого центра всасывает меньший шар вокруг того же центра.

LaTeX

$$Absorbent 𝕜 (ball p x r)$$

Lean4

@[simp]
theorem smul_ball_preimage (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜) (ha : a ≠ 0) :
    (a • ·) ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ‖a‖) :=
  Set.ext fun _ => by
    rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ← map_smul_eq_mul p, smul_sub,
      smul_inv_smul₀ ha]

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