pow_left — Mathlib

English

If f is monovary with g on s, then f^n is monovary with g on s for any natural number n.

Русский

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

LaTeX

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

Lean4

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

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