pow_mem_ball — Mathlib

English

If a ∈ ball b r, then a^n ∈ ball b^n with radius n·r, for n>0.

Русский

Если a лежит в шаре вокруг b радиуса r, то a^n лежит в шаре вокруг b^n радиуса n·r, при n>0.

LaTeX

$$$\displaystyle a^{n}\in \mathrm{ball}\,b^{n}\,(n\cdot r) \text{ for } n>0\,.$$$

Lean4

@[to_additive]
theorem pow_mem_ball {n : ℕ} (hn : 0 < n) (h : a ∈ ball b r) : a ^ n ∈ ball (b ^ n) (n • r) :=
  by
  simp only [mem_ball, dist_eq_norm_div, ← div_pow] at h ⊢
  refine lt_of_le_of_lt norm_pow_le_mul_norm ?_
  replace hn : 0 < (n : ℝ) := by norm_cast
  rw [nsmul_eq_mul]
  nlinarith

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