pow_right_injective

Mathlib.Data.Nat.Basic

URI: https://scilib.ai/kg/mathlib#Nat.pow_right_injective

English

If a ≥ 2, then the map x ↦ a^x is injective on ℕ.

Русский

Если a ≥ 2, то отображение x ↦ a^x на ℕ инъективно.

LaTeX

$$$\forall a,x,y \in \mathbb{N},\; a \ge 2 \Rightarrow a^{x}=a^{y} \Rightarrow x=y$$$

Lean4

protected theorem pow_right_injective (ha : 2 ≤ a) : Injective (a ^ ·) := by
  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru