comap — Mathlib

English

Comap along f preserves ultra-uniformity: IsUltraUniformity Y → IsUltraUniformity (u.comap f).

Русский

Перенос через f сохраняет ультра-равномерность: если Y имеет ультра-равномерность, то IsUltraUniformity (u.comap f).

LaTeX

$$$IsUltraUniformity\big( u\,\mathrm{comap}\; f \big)$$$

Lean4

theorem comap {u : UniformSpace Y} (h : IsUltraUniformity Y) (f : X → Y) : @IsUltraUniformity _ (u.comap f) :=
  by
  letI := u.comap f
  refine .mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_
  · exact fun _ ⟨_, hU, _⟩ ↦ hU.preimage_prodMap f
  · exact fun _ ⟨_, _, hU⟩ ↦ hU.preimage_prodMap f

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