English
For a collection 𝔖 of subsets of ι, the comap along the union of all elements of 𝔖, restricted to the Pi-space, equals the infimum over S ∈ 𝔖 of the comaps along S restricted to the corresponding α_i.
Русский
Для множества 𝔖 подмножеств ι, comap вдоль объединения всех элементов 𝔖, ограниченный к Pi-пространству, равен infimum по всем S ∈ 𝔖 от comap вдоль S, ограниченного к соответствующим α_i.
LaTeX
$$$UniformSpace.comap (⋃_𝔖).restrict (Pi.uniformSpace (fun i : (⋃_0 𝔖) ↦ α i)) = ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace (fun i : S ↦ α i))$$$
Lean4
theorem uniformSpace_comap_restrict_sUnion (𝔖 : Set (Set ι)) :
UniformSpace.comap (⋃₀ 𝔖).restrict (Pi.uniformSpace (fun i : (⋃₀ 𝔖) ↦ α i)) =
⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace (fun i : S ↦ α i)) :=
by
simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]
/- An infimum of complete uniformities is complete,
as long as the whole family is bounded by some common T2 topology. -/
