pow_le_pow_right_of_le_one_or_one_le

English

Let a ≥ 0. Then: if n ≤ m and a ≥ 1, or (0 ≤ a ≤ 1 and m ≤ n), then a^n ≤ a^m.

Русский

Пусть a ≥ 0. Тогда: если n ≤ m и a ≥ 1, либо (0 ≤ a ≤ 1 и m ≤ n), то a^n ≤ a^m.

LaTeX

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

Lean4

/-- `bound` lemma for branching on `1 ≤ a ∨ a ≤ 1` when proving `a ^ n ≤ a ^ m` -/
@[bound]
theorem pow_le_pow_right_of_le_one_or_one_le [ZeroLEOneClass M₀] [PosMulMono M₀]
    (h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) : a ^ n ≤ a ^ m :=
  by
  obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h
  · exact pow_right_mono₀ a1 nm
  · exact pow_le_pow_of_le_one a0 a1 mn

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