pow — Mathlib

English

If a specializes to b, then a^n specializes to b^n for every n.

Русский

Если a специализируется на b, то a^n специализируется на b^n для всех n.

LaTeX

$$$a \xrightarrow{\mathrm{Specializes}} b \Rightarrow \forall n: \mathbb{N},\ a^n \xrightarrow{\mathrm{Specializes}} b^n$$$

Lean4

@[to_additive]
protected theorem pow {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : a ⤳ b) (n : ℕ) :
    (a ^ n) ⤳ (b ^ n) :=
  Nat.recOn n (by simp only [pow_zero, specializes_rfl]) fun _ ihn ↦ by simpa only [pow_succ] using ihn.mul h

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