Product of entourages

Stream: mathlib4

[Damien Thomine]

For a separate project (topological entropy of maps), I've had to work explicitly with uniform structure and entourages, and in particular with the uniform structure on products. Then you have to convert (α × α) × β × β into (α × β) × α × β.

The current file Topology.UniformSpace.Basic just uses projections, such as

𝓤 (α × β) = comap (fun p : (α × β) × α × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β)

This is quite cumbersome when you use repeatedly such objects. I was thinking about adding an additional construction, such as

def UniformityProd (a : Set (α × α)) (b : Set (β × β)) : Set ((α × β) × α × β) :=
    { x | (x.1.1, x.2.1) ∈ a ∧ (x.1.2, x.2.2) ∈ b }

theorem UniformityProd_def {a : Set (α × α)} {b : Set (β × β)} {x : (α × β) × α × β} :
    x ∈ UniformityProd a b ↔ (x.1.1, x.2.1) ∈ a ∧ (x.1.2, x.2.2) ∈ b := by rfl

/--This one already exists; I've merely rewritten the statement with the new definition.-/
theorem mem_uniform_prod [t₁ : UniformSpace α] [t₂ : UniformSpace β] {a : Set (α × α)}
    {b : Set (β × β)} (ha : a ∈ 𝓤 α) (hb : b ∈ 𝓤 β) :
    UniformityProd a b ∈ 𝓤 (α × β) := by
  rw [uniformity_prod]; exact inter_mem_inf (preimage_mem_comap ha) (preimage_mem_comap hb)
#align mem_uniform_prod mem_uniform_prod

/--This one would be new and very convenient.-/
theorem UniformityProd_of_uniform_prod [UniformSpace α] [UniformSpace β] {s : Set ((α × β) × α × β)}
    (h : s ∈ 𝓤 (α × β)) :
    ∃ a ∈ 𝓤 α, ∃ b ∈ 𝓤 β, UniformityProd a b ⊆ s := by [...]

Questions:

• Does this makes sense, or is there already a way to manipulate painlessly such entourages?
• How could the naming above be improved?

Paging @Johannes Hölzl @Mario Carneiro @Patrick Massot

[Yaël Dillies]

Note that in Lean 4 you can write the map as fun ((a, b), (c, d)) => ((a, c), (b, d)) which makes it much more palatable in my opinion

[Eric Wieser]

Does docs#Equiv.prodProdProdComm help?

[Damien Thomine]

Thank you very much, Yaël and Eric!

I'll at least use your suggestions to clean up the current file and make it more readable. If the result is nice enough, I may avoid having to define UniformityProd (but if I do, it's no big deal).