pow_mem_closedBall — Mathlib

English

If a is within the closedBall of radius r around b, then a^n lies in the closedBall of radius n·r around b^n.

Русский

Если a находится в замкнутом шаре радиуса r вокруг b, то a^n лежит в шаре радиуса n·r вокруг b^n.

LaTeX

$$$\displaystyle a\in\mathrm{closedBall}\,b\,r \Rightarrow a^{n}\in\mathrm{closedBall}\bigl(b^{n},\,n\cdot r\bigr)$$$

Lean4

@[to_additive]
theorem pow_mem_closedBall {n : ℕ} (h : a ∈ closedBall b r) : a ^ n ∈ closedBall (b ^ n) (n • r) :=
  by
  simp only [mem_closedBall, dist_eq_norm_div, ← div_pow] at h ⊢
  refine norm_pow_le_mul_norm.trans ?_
  simpa only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg

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