smul_closedBall_preimage — Mathlib

English

A closed ball is absorbent at the origin if the radius is positive.

Русский

Замкнутый шар впитывает при положительном радиусе.

LaTeX

$$Absorbent 𝕜 (closedBall p (0:E) r)$$

Lean4

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

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