pow_monotoneOn — Mathlib

English

The map (p, q) ↦ p^q is monotone in both coordinates on {p, q ∈ ℕ × ℕ | p ≠ 0}.

Русский

Отображение (p, q) ↦ p^q монотонно по обеим координатам на множестве {p, q ∈ ℕ × ℕ | p ≠ 0}.

LaTeX

$$$\\mathrm{MonotoneOn}(\\lambda p : \\mathbb{N} \\times \\mathbb{N} \\mapsto p.1^{p.2}) \\{p \\mid p.1 \\neq 0\\}$$$

Lean4

theorem pow_monotoneOn : MonotoneOn (fun p : ℕ × ℕ ↦ p.1 ^ p.2) {p | p.1 ≠ 0} := fun _p _ _q hq hpq ↦
  (Nat.pow_le_pow_left hpq.1 _).trans (Nat.pow_le_pow_right (Nat.pos_iff_ne_zero.2 hq) hpq.2)

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