α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ 𝓢 α = Prod.map f f ⁻¹' 𝓢 β
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : inst✝² = UniformSpace.comap f inst✝¹
⊢ 𝓢 α = Prod.map f f ⁻¹' 𝓢 β
subst h
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ ⋂₀ (𝓤 α).sets = Prod.map f f ⁻¹' ⋂₀ (𝓤 β).sets
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ 𝓢 α = Prod.map f f ⁻¹' 𝓢 β
dsimp [separationRel]
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ (Prod.map f f ⁻¹' ⋂ (i : Set (β × β)) (_ : i ∈ 𝓤 β), i) = Prod.map f f ⁻¹' ⋂ (i : Set (β × β)) (_ : i ∈ (𝓤 β).sets), i
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ ⋂₀ (𝓤 α).sets = Prod.map f f ⁻¹' ⋂₀ (𝓤 β).sets
simp_rw [uniformity_comap, (Filter.comap_hasBasis (Prod.map f f) (𝓤 β)).sInter_sets, ←
  preimage_iInter, sInter_eq_biInter]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ (Prod.map f f ⁻¹' ⋂ (i : Set (β × β)) (_ : i ∈ 𝓤 β), i) = Prod.map f f ⁻¹' ⋂ (i : Set (β × β)) (_ : i ∈ (𝓤 β).sets), i
rfl