map_pow_le_pow' — Mathlib

English

If p(1) ≤ 1, then p(a^n) ≤ p(a)^n for all n ≥ 0.

Русский

Если p(1) ≤ 1, то для всех n ≥ 0 выполняется p(a^n) ≤ p(a)^n.

LaTeX

$$$\forall n : \mathbb{N},\ p(a^n) \le p(a)^n$$$

Lean4

/-- If `f` is a ring seminorm on `a` with `f 1 ≤ 1`, then `∀ (n : ℕ), f (a ^ n) ≤ f a ^ n`. -/
theorem map_pow_le_pow' {F α : Type*} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {f : F} (hf1 : f 1 ≤ 1)
    (a : α) : ∀ n : ℕ, f (a ^ n) ≤ f a ^ n
  | 0 => by simp only [pow_zero, hf1]
  | n + 1 => by
    simp only [pow_succ _ n]
    exact le_trans (map_mul_le_mul f _ a) (mul_le_mul_of_nonneg_right (map_pow_le_pow' hf1 _ n) (apply_nonneg f a))

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