pow_right

Mathlib.Algebra.Order.Monovary

URI: https://scilib.ai/kg/mathlib#Antivary.pow_right

English

If hfg is AntivaryOn f g s, then for all n, AntivaryOn f (g^n) s.

Русский

Если hfg = AntivaryOn f g s, то для каждого n верно AntivaryOn f (g^n) s.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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