pow_lt_one₀ — Mathlib

English

Let a ∈ M₀ with 0 ≤ a < 1. Then for every n ≠ 0, a^n < 1.

Русский

Пусть a ∈ M₀, 0 ≤ a < 1. Тогда для любого n ≠ 0, a^n < 1.

LaTeX

$$$ 0 \\le a \\land a < 1 \\Rightarrow \\forall n \\; (n \\neq 0) \\Rightarrow a^n < 1 $$$

Lean4

theorem pow_lt_one₀ [PosMulMono M₀] (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < 1
  | 0, h => (h rfl).elim
  | n + 1, _ => by rw [pow_succ']; exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

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