English
For monotone g, if ((𝓤 α).lift (λ s, g (preimage Prod.swap s))) ≤ f, then (𝓤 α).lift g ≤ f.
Русский
Если g монотонна и выполняется неравенство с lift и preimage Prod.swap, то выполнить неравенство с lift g.
LaTeX
$$$$\\text{If } g\\text{ is monotone and } ( (𝓤 α).lift (\\lambda s, g (\\text{preimage} (Prod.swap) s)) ) \\le f,\\; \\text{then } (𝓤 α).lift g \\le f.$$$$
Lean4
theorem uniformity_lift_le_swap {g : Set (α × α) → Filter β} {f : Filter β} (hg : Monotone g)
(h : ((𝓤 α).lift fun s => g (preimage Prod.swap s)) ≤ f) : (𝓤 α).lift g ≤ f :=
calc
(𝓤 α).lift g ≤ (Filter.map (@Prod.swap α α) <| 𝓤 α).lift g := lift_mono uniformity_le_symm le_rfl
_ ≤ _ := by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h
