English
Let 𝔖 be a family of subsets of α with a covering property, and φ1, φ2 map domains δ1, δ2 to α with given index families 𝔗1, 𝔗2. If every S ∈ 𝔖 is contained in range φ1 ∪ range φ2 and the images/preimages realize 𝔖 via 𝔗1 and 𝔗2, then the uniform structure on α induced by 𝔖 equals the infimum of the two uniform structures obtained by precomposing with φ1 and φ2 (through the corresponding 𝔗’s).
Русский
Пусть 𝔖 — семейство подмножеств α с покрытием, и даны отображения φ1: δ1 → α, φ2: δ2 → α с семействами 𝔗1, 𝔗2 таких, что S ⊆ range φ1 ∪ range φ2 для каждого S ∈ 𝔖 и соответствующие условия на изображения/предобразования реализуют 𝔖 через 𝔗1, 𝔗2. ТогдаUniformSpace на α, заданный 𝔖, равенInfimum двух UniformSpaces, получаемых вытягиванием через φ1 и φ2 по 𝔗1, 𝔗2.
LaTeX
$$$\\mathcal{V}(\\alpha, \\beta, \\mathfrak{S}) = \\operatorname{comap}(\\text{ofFun } \\mathcal{T}_1 \\circ (\\cdot \\circ \\varphi_1) \\circ \\text{toFun } \\mathfrak{S})\\, \\mathcal{V}(\\delta_1, \\beta, \\mathcal{T}_1) \\;\\sqcap\\; \\operatorname{comap}(\\text{ofFun } \\mathcal{T}_2 \\circ (\\cdot \\circ \\varphi_2) \\circ \\text{toFun } \\mathfrak{S})\\, \\mathcal{V}(\\delta_2, \\beta, \\mathcal{T}_2) $$$
Lean4
theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁))
(𝔗₂ : Set (Set δ₂)) (h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖) (h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖)
(h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁) (h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂)
(h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂) :
𝒱(α, β, 𝔖, _) =
.comap (ofFun 𝔗₁ ∘ (· ∘ φ₁) ∘ toFun 𝔖) 𝒱(δ₁, β, 𝔗₁, _) ⊓ .comap (ofFun 𝔗₂ ∘ (· ∘ φ₂) ∘ toFun 𝔖) 𝒱(δ₂, β, 𝔗₂, _) :=
by
set ψ₁ : Π S : Set α, φ₁ ⁻¹' S → S := fun S ↦ S.restrictPreimage φ₁
set ψ₂ : Π S : Set α, φ₂ ⁻¹' S → S := fun S ↦ S.restrictPreimage φ₂
have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = .comap (· ∘ ψ₁ S) 𝒰(_, β, _) ⊓ .comap (· ∘ ψ₂ S) 𝒰(_, β, _) :=
by
refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_
simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union, ← image_subset_iff, image_univ,
Subtype.range_val] using h_cover S hS
refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)
· rw [← uniformContinuous_iff]
exact UniformOnFun.precomp_uniformContinuous h_image₁
· rw [← uniformContinuous_iff]
exact UniformOnFun.precomp_uniformContinuous h_image₂
· simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf, ← UniformSpace.comap_comap]
exact inf_le_inf (iInf₂_le_of_le _ (h_preimage₁ hS) le_rfl) (iInf₂_le_of_le _ (h_preimage₂ hS) le_rfl)
