norm_lt_pow_iff_norm_le_pow_sub_one

English

For x ∈ ℚ_p and n ∈ ℤ, the equivalence of norm inequalities with shifted exponent holds: norm ≤ p^n iff norm < p^{n−1} under appropriate interpretation.

Русский

Для x ∈ ℚ_p и n ∈ ℤ равносильность норм сдвинутых степеней: ‖x‖ ≤ p^n эквивалентно ‖x‖ < p^{n−1}.

LaTeX

$$‖x‖ ≤ p^n \Leftrightarrow ‖x‖ < p^{n-1}$$

Lean4

theorem norm_lt_pow_iff_norm_le_pow_sub_one (x : ℚ_[p]) (n : ℤ) : ‖x‖ < (p : ℝ) ^ n ↔ ‖x‖ ≤ (p : ℝ) ^ (n - 1) := by
  rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

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