uniformSpace_comap_precomp — Mathlib

English

For a subset S ⊆ ι, the comap of the Pi-space along the restriction S.restrict equals the infimum over i ∈ S of comap along eval i of U i.

Русский

Для подмножества S ⊆ ι равномерная структура пространства Pi после ограничения S.restrict равна infimum по i ∈ S от comap по eval i на U_i.

LaTeX

$$$UniformSpace.comap (S.restrict) (Pi.uniformSpace (fun i : S \\mapsto \\alpha i)) = ⨅ i ∈ S, UniformSpace.comap (eval i) (U i)$$$

Lean4

theorem uniformSpace_comap_precomp (φ : ι' → ι) :
    UniformSpace.comap (· ∘ φ) (Pi.uniformSpace (fun _ ↦ β)) =
      ⨅ i', UniformSpace.comap (eval (φ i')) ‹UniformSpace β› :=
  uniformSpace_comap_precomp' (fun _ ↦ β) φ

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