pow_right_injective — Mathlib

English

If a ∈ ℤ with natAbs(a) > 1, the map x ↦ a^x from ℕ to ℤ is injective.

Русский

Если |a| > 1 для a ∈ ℤ, то отображение x ↦ a^x: ℕ → ℤ инъективно.

LaTeX

$$$$ \\text{pow\_right\_injective}(a) : \\bigl\\{ {\\, a^x \\}_{x \\in \\mathbb{N}} \\bigr\\} \\text{ инъективно при } 1 < |a| $$$$

Lean4

theorem pow_right_injective (h : 1 < a.natAbs) : ((a ^ ·) : ℕ → ℤ).Injective :=
  by
  refine (?_ : (natAbs ∘ (a ^ · : ℕ → ℤ)).Injective).of_comp
  convert Nat.pow_right_injective h using 2
  rw [Function.comp_apply, natAbs_pow]

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