English
Let φ: δ → α, 𝔗 a family of coverings of δ, and h_image/h_preimage express how the coverings map to 𝔖. If 𝔖 is coverable by finite unions of ranges of φ, then the uniform space on α with respect to 𝔖 equals the infimum over i of the comaps of the uniform spaces on δi via the precomposition with φi and the i-th 𝔗i.
Русский
Пусть φ: δ → α, 𝔗 семейство покрытий δ, и условия отображения/предобразования задают 𝔖. Если 𝔖 можно покрить конечной объединением диапазонов φi, то UniformSpace на α относительно 𝔖 равен инфимума по i от comap(…) 𝒱(δi, β, 𝔗i).
LaTeX
$$$\\mathcal{V}(\\alpha, β, 𝔖) = \\bigwedge_{i} \\operatorname{comap}(\\text{ofFun } (\\mathcal{T}_i) \\circ (\\cdot \\circ φ_i) \\circ toFun 𝔖) \\mathcal{V}(δ_i, β, 𝔗_i)$$$
Lean4
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ i → α) (𝔗 : ∀ i, Set (Set (δ i)))
(h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖) (h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i))
(h_cover : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)) :
𝒱(α, β, 𝔖, _) = ⨅ i, .comap (ofFun (𝔗 i) ∘ (· ∘ φ i) ∘ toFun 𝔖) 𝒱(δ i, β, 𝔗 i, _) :=
by
set ψ : Π S : Set α, Π i : ι, (φ i) ⁻¹' S → S := fun S i ↦ S.restrictPreimage (φ i)
have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = ⨅ i, .comap (· ∘ ψ S i) 𝒰(_, β, _) := fun S hS ↦
by
rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩
simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂, ← image_subset_iff, image_univ,
Subtype.range_val] using I_cover
refine le_antisymm (le_iInf fun i ↦ ?_) (le_iInf₂ fun S hS ↦ ?_)
· rw [← uniformContinuous_iff]
exact UniformOnFun.precomp_uniformContinuous (h_image i)
· simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl
