pow_right — Mathlib

English

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

Русский

Если f антивариантна по отношению к g на s, то для любого натурального n 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 : AntivaryOn f g s) (n : ℕ) : AntivaryOn f (g ^ n) s := fun _i hi _j hj hij ↦
  hfg hi hj <| lt_of_pow_lt_pow_left' _ hij

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