pow_left — Mathlib

English

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

Русский

Если f антивариантно варьируется с g на s, то f^n антивариантно варьируется с g на s для каждого натурального n.

LaTeX

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

Lean4

@[to_additive]
theorem pow_left (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn (f ^ n) g s := fun _i hi _j hj hij ↦
  pow_le_pow_left' (hfg hi hj hij) _

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