pow_monotone — Mathlib

English

Let a be an element of a C*-algebra A with a ≥ 1. Then the map n ↦ a^n is monotone in n: if n ≤ m then a^n ≤ a^m.

Русский

Пусть a ∈ A satisfies a ≥ 1; тогда отображение n ↦ a^n монотонно по n: если n ≤ m, то a^n ≤ a^m.

LaTeX

$$$a \\ge 1 \\Rightarrow (n \\mapsto a^{n}) \\text{ is Monotone on } \\mathbb{N}.$$$

Lean4

theorem pow_monotone {a : A} (ha : 1 ≤ a) : Monotone (a ^ · : ℕ → A) :=
  by
  have ha' : 0 ≤ a := zero_le_one.trans ha
  intro n m hnm
  simp only
  rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
  rw [CFC.one_le_iff (R := ℝ) a] at ha
  peel ha with x hx _
  exact pow_le_pow_right₀ (ha x hx) hnm

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