α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.155123
t₁ : UniformSpace α
t₂ : UniformSpace β
a : Set (α × α)
b : Set (β × β)
ha : a ∈ 𝓤 α
hb : b ∈ 𝓤 β
⊢ {p | (p.fst.fst, p.snd.fst) ∈ a ∧ (p.fst.snd, p.snd.snd) ∈ b} ∈
    comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 α) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.155123
t₁ : UniformSpace α
t₂ : UniformSpace β
a : Set (α × α)
b : Set (β × β)
ha : a ∈ 𝓤 α
hb : b ∈ 𝓤 β
⊢ {p | (p.fst.fst, p.snd.fst) ∈ a ∧ (p.fst.snd, p.snd.snd) ∈ b} ∈ 𝓤 (α × β)
rw [uniformity_prod]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.155123
t₁ : UniformSpace α
t₂ : UniformSpace β
a : Set (α × α)
b : Set (β × β)
ha : a ∈ 𝓤 α
hb : b ∈ 𝓤 β
⊢ {p | (p.fst.fst, p.snd.fst) ∈ a ∧ (p.fst.snd, p.snd.snd) ∈ b} ∈
    comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 α) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 β)
exact inter_mem_inf (preimage_mem_comap ha) (preimage_mem_comap hb)