uniformContinuous_zpow_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive uniformContinuous_const_zsmul]
theorem uniformContinuous_zpow_const (n : ℤ) : UniformContinuous fun x : α => x ^ n :=
  uniformContinuous_id.zpow_const n

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