α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49944
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap ⁻¹' V ∈ (𝓤 α).sets
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49944
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ symmetrizeRel V ∈ 𝓤 α
apply (𝓤 α).inter_sets h
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49944
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap '' V ∈ (Prod.swap <$> 𝓤 α).sets
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49944
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap ⁻¹' V ∈ (𝓤 α).sets
rw [← image_swap_eq_preimage_swap, uniformity_eq_symm]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49944
inst✝ : UniformSpace α
V : Set (α × α)
h : V ∈ 𝓤 α
⊢ Prod.swap '' V ∈ (Prod.swap <$> 𝓤 α).sets
exact image_mem_map h