le_self_pow_of_pos — Mathlib

English

Let a ≥ 0 with a ≤ 1. Then for m ≤ n, a^n ≤ a^m.

Русский

Пусть a ≥ 0 и a ≤ 1. Тогда при m ≤ n выполняется a^n ≤ a^m.

LaTeX

$$$ [(0 \\le a) \\land (a \\le 1) \\land (m \\le n)] \\Rightarrow a^n \\le a^m $$$

Lean4

/-- The `bound` tactic can't handle `m ≠ 0` goals yet, so we express as `0 < m` -/
@[bound]
theorem le_self_pow_of_pos [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 1 ≤ a) (hn : 0 < n) : a ≤ a ^ n :=
  le_self_pow₀ ha hn.ne'

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