α : Type u_1
β : Type u_2
γ : Type ?u.63791
ι : Type ?u.63794
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ map
      (fun x =>
        ((↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.fst, (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) ≤
    𝓤 (↑s →ᵤ β)
α : Type u_1
β : Type u_2
γ : Type ?u.63791
ι : Type ?u.63794
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ UniformContinuous (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖))
change _ ≤ _
α : Type u_1
β : Type u_2
γ : Type ?u.63791
ι : Type ?u.63794
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ (⨅ (i : Set α) (_ : i ∈ 𝔖), 𝓤 (α →ᵤ[𝔖] β)) ≤
    comap
      (fun x =>
        ((↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.fst, (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (↑s →ᵤ β))
α : Type u_1
β : Type u_2
γ : Type ?u.63791
ι : Type ?u.63794
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ map
      (fun x =>
        ((↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.fst, (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) ≤
    𝓤 (↑s →ᵤ β)
simp only [UniformOnFun.uniformSpace, map_le_iff_le_comap, iInf_uniformity]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.63791
ι : Type ?u.63794
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ (⨅ (i : Set α) (_ : i ∈ 𝔖), 𝓤 (α →ᵤ[𝔖] β)) ≤
    comap
      (fun x =>
        ((↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.fst, (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (↑s →ᵤ β))
exact iInf₂_le s h