isUltraUniformity — Mathlib

English

If f: X → Y is uniformly inducing and Y has an ultra uniformity, then X has an ultra uniformity.

Русский

Если f: X → Y является равномерно-индуцирующим отображением и Y имеет ультра-однородность, то X также имеет ультра-однородность.

LaTeX

$$$[IsUltraUniformity Y] \Rightarrow IsUltraUniformity X$ via IsUniformInducing f$$

Lean4

theorem isUltraUniformity [IsUltraUniformity Y] {f : X → Y} (hf : IsUniformInducing f) : IsUltraUniformity X :=
  hf.comap_uniformSpace ▸ .comap inferInstance f

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