pow_right_strictMono — Mathlib

English

The function a ↦ a^n is strictly monotone on WithTop α for any fixed n ≠ 0, given appropriate order and algebraic conditions.

Русский

Функция a ↦ a^n строго возрастает на WithTop α при фиксированном n ≠ 0 и при соответствующем порядке и алгебраических условиях.

LaTeX

$$$\\\\forall n \\\\neq 0,\\\\\\;\\\\text{StrictMono}(\\\\lambda a, a^n)$$$

Lean4

protected theorem pow_right_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a : WithTop α ↦ a ^ n
  | 0, h => absurd rfl h
  | 1, _ => by simpa only [pow_one] using strictMono_id
  | n + 2, _ => fun x y h ↦ by
    simp_rw [pow_succ _ (n + 1)]
    exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h

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