one_le_pow_of_le — Mathlib

English

Let M be a monoid with a compatible preorder and MulLeftMono. If a ≥ 1, then a^n ≥ 1 for every n ∈ ℕ.

Русский

Пусть имеется моноид M с совместимым порядком и левая монотонность умножения. Если a ≥ 1, то a^n ≥ 1 для всех n ∈ ℕ.

LaTeX

$$1 ≤ a ⇒ ∀ n ∈ ℕ, 1 ≤ a^n$$

Lean4

@[to_additive Left.nsmul_nonneg]
theorem one_le_pow_of_le (ha : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n
  | 0 => by simp
  | k + 1 => by
    rw [pow_succ]
    exact one_le_mul (one_le_pow_of_le ha k) ha

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