nat_pow

Mathlib.Algebra.Order.Group.Nat

URI: https://scilib.ai/kg/mathlib#StrictMono.nat_pow

English

If f is strictly monotone and n ≠ 0, then x ↦ f(x)^n is strictly monotone.

Русский

Если f строго монотонна и n ≠ 0, тогда x ↦ f(x)^n строго монотонно по x.

LaTeX

$$$n \neq 0 \land \text{StrictMono}(f) \Rightarrow \text{StrictMono}(x \mapsto f(x)^n).$$$

Lean4

theorem _root_.StrictMono.nat_pow [Preorder α] (hn : n ≠ 0) (hf : StrictMono f) : StrictMono (f · ^ n) :=
  (Nat.pow_left_strictMono hn).comp hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru