α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q => (↑q.fst, ↑q.snd)) ∘ fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 α) =
    comap (fun q => (↑q.fst, ↑q.snd)) (𝓤 α)
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap (fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 ↑t) = 𝓤 ↑s
rw [uniformity_subtype, uniformity_subtype, comap_comap]
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q => (↑q.fst, ↑q.snd)) ∘ fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 α) =
    comap (fun q => (↑q.fst, ↑q.snd)) (𝓤 α)
rfl