epow_left_mono — Mathlib

English

For a fixed exponent y, the map x ↦ x^y is monotone in x.

Русский

При фиксированном показателе y отображение x ↦ x^y монотонно по x.

LaTeX

$$$ \forall y \in \mathbb{N}_\infty,\; \text{Monotone}(x \mapsto x^y). $$$

Lean4

theorem epow_left_mono : Monotone (fun x : ℕ∞ ↦ x ^ y) :=
  by
  intro x z x_z
  simp only
  induction y
  · rcases lt_trichotomy x 1 with x_0 | rfl | x_2
    · rw [lt_one_iff_eq_zero.1 x_0, zero_epow_top]; exact bot_le
    · rw [one_epow]; exact one_le_epow (one_le_iff_ne_zero.1 x_z)
    · rw [epow_top (x_2.trans_le x_z)]; exact le_top
  · simp only [epow_natCast, (pow_left_mono _) x_z]

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