case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ comap (fun x => ((↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.fst, (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.snd))
      (𝓤 (α →ᵤ β)) =
    𝓤 (α →ᵤ γ)
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ UniformInducing (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun)
constructor
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (fun x => ((↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.fst, (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.snd))
      (𝓤 (α →ᵤ β)) =
    𝓤 (α →ᵤ γ)
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ comap (fun x => ((↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.fst, (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.snd))
      (𝓤 (α →ᵤ β)) =
    𝓤 (α →ᵤ γ)
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (Prod.map (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun)) (𝓤 (α →ᵤ β)) = 𝓤 (α →ᵤ γ)
rw [← uniformity_comap] at hf⊢
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β) = uniformSpace α γ
case comap_uniformity
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
congr
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β) =
    UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β) = uniformSpace α γ
rw [← uniformSpace_eq hf, UniformFun.comap_eq]
no goals
case comap_uniformity.h.e_2.h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.40608
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β) =
    UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
rfl