α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.50331
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : (Filter.lift (𝓤 α) fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ Filter.lift (𝓤 α) (g ∘ preimage Prod.swap) ≤ f
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.50331
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : (Filter.lift (𝓤 α) fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ Filter.lift (map Prod.swap (𝓤 α)) g ≤ f
rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.50331
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : (Filter.lift (𝓤 α) fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ Filter.lift (𝓤 α) (g ∘ preimage Prod.swap) ≤ f
exact h