English
The uniformity of α →ᵤ γ at the infimum of a family (⨅ i, u_i) equals the infimum of the induced uniformities: 𝒰(α, γ, ⨅ i, u_i) = ⨅ i, 𝒰(α, γ, u_i).
Русский
Равномерность на α →ᵤ γ при инфимумации семейства u_i равна инфимумау одновременных равномерностей: 𝒰(α, γ, ⨅ i, u_i) = ⨅ i, 𝒰(α, γ, u_i).
LaTeX
$$$$ 𝒰(α, γ, (\bigwedge_i u_i)) = \bigwedge_i 𝒰(α, γ, u_i). $$$$
Lean4
/-- If `u` is a family of uniform structures on `γ`, then
`𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)`. -/
protected theorem iInf_eq {u : ι → UniformSpace γ} : 𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i) := by
-- This follows directly from the fact that the upper adjoint in a Galois connection maps
-- infimas to infimas.
ext : 1
change UniformFun.filter α γ 𝓤[⨅ i, u i] = 𝓤[⨅ i, 𝒰(α, γ, u i)]
rw [iInf_uniformity, iInf_uniformity]
exact (UniformFun.gc α γ).u_iInf
