zpow_const — Mathlib

English

The uniformity on α equals the comap of the neighborhood filter at 1 under the map (x, y) ↦ y/x.

Русский

Унииформность на α равна обратному образу фильтра соседних окрестностей в единице по отображению (x, y) ↦ y/x.

LaTeX

$$$\\mathcal{U}(\\alpha) = \\mathrm{comap}\\bigl(\\lambda x:(\\alpha \\times \\alpha).\\, x_2 / x_1\\bigr)(\\mathcal{N}(1))$$$

Lean4

@[to_additive UniformContinuous.const_zsmul]
theorem zpow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : ∀ n : ℤ, UniformContinuous fun x => f x ^ n
  | (n : ℕ) => by
    simp_rw [zpow_natCast]
    exact hf.pow_const _
  | Int.negSucc n => by
    simp_rw [zpow_negSucc]
    exact (hf.pow_const _).inv

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