English
A more general formulation of the previous result: for ι, α, 𝔖 a set of sets of ι, the comap over 𝔖.sUnion restricted to the Pi-space equals the iterated infimum over S ∈ 𝔖 of the comaps along S.restrict.
Русский
Обобщение предыдущего результата: для ι, α и 𝔖 — множество подмножеств ι, comap 𝔖.sUnion.restrict к Pi-пространству равен итеративному infimum по S ∈ 𝔖 от comap по S.restrict.
LaTeX
$$$UniformSpace.comap 𝔖.sUnion.restrict (Pi.uniformSpace (fun i => α i.val)) = iInf (fun S => iInf (fun h => UniformSpace.comap S.restrict (Pi.uniformSpace (fun i => α i.val))))$$$
Lean4
protected theorem iInf {ι X : Type*} {u : ι → UniformSpace X} (hu : ∀ i, @CompleteSpace X (u i))
(ht : ∃ t, @T2Space X t ∧ ∀ i, (u i).toTopologicalSpace ≤ t) : @CompleteSpace X (⨅ i, u i) := by
-- We can assume `X` is nonempty.
nontriviality X
rcases ht with
⟨t, ht, hut⟩
-- The diagonal map `(X, ⨅ i, u i) → ∀ i, (X, u i)` is a uniform embedding.
have : @IsUniformInducing X (ι → X) (⨅ i, u i) (Pi.uniformSpace (U := u)) (const ι) := by
simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf, Filter.comap_comap, comp_def,
const, Prod.eta, comap_id']
-- Hence, it suffices to show that its range, the diagonal, is closed in `Π i, (X, u i)`.
simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal, setOf_forall]
-- The separation of `t` ensures that this is the case in `Π i, (X, t)`, hence the result
-- since the topology associated to each `u i` is finer than `t`.
have : Pi.topologicalSpace (t₂ := fun i ↦ (u i).toTopologicalSpace) ≤ Pi.topologicalSpace (t₂ := fun _ ↦ t) :=
iInf_mono fun i ↦ induced_mono <| hut i
refine IsClosed.isComplete <| .mono ?_ this
exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦ isClosed_eq (continuous_apply _) (continuous_apply _)
