English
For x ≠ 0, the map y ↦ x^y is monotone on ENat.
Русский
При x ≠ 0 отображение y ↦ x^y монотонно по отношению к y на ENat.
LaTeX
$$$ \forall x \in \mathbb{N}_\infty,\; x \neq 0 \Rightarrow \forall y,z \in \mathbb{N}_\infty,\; y \le z \Rightarrow x^{y} \le x^{z}. $$$
Lean4
theorem epow_right_mono (h : x ≠ 0) : Monotone (fun y : ℕ∞ ↦ x ^ y) :=
by
intro y z y_z
induction y
· rw [top_le_iff.1 y_z]
induction z
· rcases lt_trichotomy x 1 with x_0 | rfl | x_2
· exact (h (lt_one_iff_eq_zero.1 x_0)).rec
· simp only [one_epow, le_refl]
· simp only [epow_top x_2, le_top]
· exact pow_right_mono₀ (one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)
