pow_right_injective₀ — Mathlib

English

If a > 0 and a ≠ 1, then the map x ↦ a^x is injective on natural numbers.

Русский

Если a > 0 и a ≠ 1, то отображение x ↦ a^x по натуральным числам инъективно.

LaTeX

$$$0 < a \land a \neq 1 \Rightarrow (\forall m,n\in\mathbb{N})\ a^m = a^n \Rightarrow m = n$$$

Lean4

theorem pow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·) :=
  by
  obtain ha₁ | ha₁ := ha₁.lt_or_gt
  · exact (pow_right_strictAnti₀ ha₀ ha₁).injective
  · exact (pow_right_strictMono₀ ha₁).injective

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