uniformSpace_comap_restrict — Mathlib

English

For S ⊆ ι, the comap of the restricted Pi-space equals the infimum over i ∈ S of comap along eval i.

Русский

Для подмножества S ⊆ ι комап ограниченного Pi-пространства равен инфимууму по i∈S от comap по eval 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_restrict (S : Set ι) :
    UniformSpace.comap (S.restrict) (Pi.uniformSpace (fun i : S ↦ α i)) = ⨅ i ∈ S, UniformSpace.comap (eval i) (U i) :=
  by simp +unfoldPartialApp [← iInf_subtype'', ← uniformSpace_comap_precomp' _ ((↑) : S → ι), Set.restrict]

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