α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) β)) ≤
    ⨅ (i : Set γ) (_ : i ∈ 𝔗),
      UniformSpace.comap (restrict i ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑i) β)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
⊢ UniformContinuous fun g => ↑(ofFun 𝔗) (g ∘ f)
simp_rw [uniformContinuous_iff, UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ←
  UniformSpace.comap_comap]
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) β)) ≤
    ⨅ (i : Set γ) (_ : i ∈ 𝔗),
      UniformSpace.comap (restrict i ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑i) β)
refine' le_iInf₂ fun t ht => iInf_le_of_le (f '' t) <| iInf_le_of_le (hf ht) _
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
let f' : t → f '' t := (mapsTo_image f t).restrict f t (f '' t)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
have :
  (t.restrict ∘ fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (g ∘ f)) =
    (fun g : f '' t → β => g ∘ f') ∘ (f '' t).restrict :=
  rfl
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict (f '' t)) (UniformSpace.comap (fun g => g ∘ f') (UniformFun.uniformSpace (↑t) β))
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
rw [this, @UniformSpace.comap_comap (α →ᵤ[𝔖] β) (f '' t →ᵤ β)]
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformFun.uniformSpace (↑(f '' t)) β ≤ UniformSpace.comap (fun g => g ∘ f') (UniformFun.uniformSpace (↑t) β)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict (f '' t)) (UniformSpace.comap (fun g => g ∘ f') (UniformFun.uniformSpace (↑t) β))
refine' UniformSpace.comap_mono _
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformContinuous fun g => g ∘ f'
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformFun.uniformSpace (↑(f '' t)) β ≤ UniformSpace.comap (fun g => g ∘ f') (UniformFun.uniformSpace (↑t) β)
rw [← uniformContinuous_iff]
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.81138
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformContinuous fun g => g ∘ f'
exact UniformFun.precomp_uniformContinuous