pow_right — Mathlib

English

If f monovaries with g on s, then for every natural number n, f monovaries with g^n on s.

Русский

Если f мономорфна по отношению к g на s, то для любого натурального числа n f мономорфна по отношению к g^n на s.

LaTeX

$$$ MonovaryOn f g s \Rightarrow \forall n \in \mathbb{N}, MonovaryOn f (g^n) s $$$

Lean4

@[to_additive]
theorem pow_right (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn f (g ^ n) s := fun _i hi _j hj hij ↦
  hfg hi hj <| lt_of_pow_lt_pow_left' _ hij

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