case h
α : Type u_1
β : Type u_2
γ : Type ?u.53041
ι : Type ?u.53044
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    uv ∈ Prod.map (restrict S ∘ ↑UniformFun.toFun) (restrict S ∘ ↑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
α : Type u_1
β : Type u_2
γ : Type ?u.53041
ι : Type ?u.53044
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
⊢ UniformOnFun.gen 𝔖 S V =
    Prod.map (restrict S ∘ ↑UniformFun.toFun) (restrict S ∘ ↑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
ext uv
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.53041
ι : Type ?u.53044
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    uv ∈ Prod.map (restrict S ∘ ↑UniformFun.toFun) (restrict S ∘ ↑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩