English
On the product of filters, map Prod.mk f and g commute with seq up to a symmetrized form: (map Prod.mk f).seq g = seq (map (λ b a. (a,b)) g) f.
Русский
Для произведения фильтров отображение Prod.mk f и g коммутируют с seq до симметричной формы: (map Prod.mk f).seq g = seq (map (λ b a. (a,b)) g) f.
LaTeX
$$$ (\operatorname{map} \operatorname{Prod.mk} f).\text{seq} g = \text{seq} (\operatorname{map} (\lambda b\, a. (a,b)) g) f $$$
Lean4
theorem prod_map_seq_comm (f : Filter α) (g : Filter β) : (map Prod.mk f).seq g = seq (map (fun b a => (a, b)) g) f :=
by
refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
· rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
refine mem_of_superset ?_ (Set.seq_mono hs Subset.rfl)
rw [← Set.prod_image_seq_comm]
exact seq_mem_seq (image_mem_map ht) hu
· rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
refine mem_of_superset ?_ (Set.seq_mono hs Subset.rfl)
rw [Set.prod_image_seq_comm]
exact seq_mem_seq (image_mem_map ht) hu
