pow_left — Mathlib

English

If f antivaries with g on s, then f^n antivaries with g on s for all natural numbers 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 : Antivary f g) (n : ℕ) : Antivary (f ^ n) g := fun _i _j hij ↦ pow_le_pow_left' (hfg hij) _

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