Lean4
/-- Given `f : α → β` and a uniformity `u` on `β`, the inverse image of `u` under `f`
is the inverse image in the filter sense of the induced function `α × α → β × β`.
See note [reducible non-instances]. -/
abbrev comap (f : α → β) (u : UniformSpace β) : UniformSpace α
where
uniformity := 𝓤[u].comap fun p : α × α => (f p.1, f p.2)
symm := by
simp only [tendsto_comap_iff]
exact tendsto_swap_uniformity.comp tendsto_comap
comp :=
le_trans
(by
rw [comap_lift'_eq, comap_lift'_eq2]
· exact lift'_mono' fun s _ ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩ => ⟨f x, h₁, h₂⟩
· exact monotone_id.compRel monotone_id)
(comap_mono u.comp)
toTopologicalSpace := u.toTopologicalSpace.induced f
nhds_eq_comap_uniformity x := by simp only [nhds_induced, nhds_eq_comap_uniformity, comap_comap, Function.comp_def]
