English
If φ_i : δ_i → α cover α, then 𝒰(α, β) equals the infimum of comaps of each δ_i, i.e., 𝒰(α, β) = inf_i 𝒰(δ_i, β) comapped appropriately.
Русский
При покрытии α функциями φ_i равномерность α равна инфимума соответствующих обобщений по δ_i.
LaTeX
$$$$ 𝒰(α, β) = \inf_i \; \mathrm{comap}(\mathrm{ofFun} \circ (· \circ φ_i) \circ toFun) 𝒰(δ_i, β). $$$$
Lean4
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ i → α)
(h_cover : ∃ I : Set ι, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ) :
𝒰(α, β, _) = ⨅ i, .comap (ofFun ∘ (· ∘ φ i) ∘ toFun) 𝒰(δ i, β, _) :=
by
ext : 1
simp_rw [iInf_uniformity, uniformity_comap]
refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_
rcases h_cover with ⟨I, I_finite, I_cover⟩
refine
HasBasis.iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _) |>.le_basis_iff
(UniformFun.hasBasis_uniformity α β) |>.mpr
fun U hU ↦ ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩
exact mem_iInter.mp hfg ⟨i, hi⟩ y
