∀ {α : Type u_1} {β : Type u_2} (f : α → β) (u : UniformSpace β),
  ((Filter.comap (fun p => (f p.1, f p.2)) (uniformity β)).lift' fun s => SetRel.comp s s) ≤
    Filter.comap (fun p => (f p.1, f p.2)) (uniformity β)