English
If s is a spaced-out subset of β×β (not intersecting with the image of a map f on distinct points), then comap of the uniformity is the discrete one on α.
Русский
Если s является разбросанным по β×β подмножеством и не пересекается с образом пары (f x, f y) при x≠y, то композиция обобщает дискретность на α.
LaTeX
$$$\\text{comap} (Prod.map f f) (\\mathcal{U}(\\beta)) = \\mathcal{P}(idRel)$ under spaced-out condition$$
Lean4
/-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed
`s ∈ 𝓤 β`, then `f` is uniform inducing with respect to the discrete uniformity on `α`:
the preimage of `𝓤 β` under `Prod.map f f` is the principal filter generated by the diagonal in
`α × α`. -/
theorem comap_uniformity_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
(hf : Pairwise fun x y => (f x, f y) ∉ s) : comap (Prod.map f f) (𝓤 β) = 𝓟 idRel :=
by
refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))
calc
comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
_ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
_ ≤ 𝓟 idRel := principal_mono.2 ?_
rintro ⟨x, y⟩; simpa [not_imp_not] using @hf x y
