English
If there is a finite cover of α by ranges of φ_i, then 𝒰(α, β) equals the infimum of comaps along φ_i of 𝒰(δ_i, β).
Русский
Если существует конечное покрытие α диапазонами φ_i, то 𝒰(α, β) равно инфимумаии по i от comap φ_i 𝒰(δ_i, β).
LaTeX
$$$$ 𝒰(α, β) = \inf_i \mathrm{comap}(\mathrm{ofFun} \circ (· \circ φ_i) \circ toFun) 𝒰(δ_i, β). $$$$
Lean4
theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α)
(h_cover : range φ₁ ∪ range φ₂ = univ) :
𝒰(α, β, _) = .comap (ofFun ∘ (· ∘ φ₁) ∘ toFun) 𝒰(δ₁, β, _) ⊓ .comap (ofFun ∘ (· ∘ φ₂) ∘ toFun) 𝒰(δ₂, β, _) :=
by
ext : 1
refine le_antisymm (le_inf ?_ ?_) ?_
· exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
· exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
· refine
(UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
(UniformFun.hasBasis_uniformity δ₂ β |>.comap _) |>.le_basis_iff
(UniformFun.hasBasis_uniformity α β) |>.mpr
fun U hU ↦ ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩ | ⟨y, rfl⟩)
· exact hfg.1 y
· exact hfg.2 y
