English
Let f be a closed map and continuous. For any filter F on X, the lift of closure commutes with pushforward along f: (map f F).lift' closure = map f (F.lift' closure).
Русский
Пусть f — замкнутое отображение и непрерывное. Для любого фильтра F на X отображение замыкания и предобразования по f commute: (map f F).lift' closure = map f (F.lift' closure).
LaTeX
$$$ (\operatorname{map} f F).\mathrm{lift}'(\mathrm{closure}) = \operatorname{map} f (F.\mathrm{lift}'(\mathrm{closure})) $$$
Lean4
theorem lift'_closure_map_eq (f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter X) :
(map f F).lift' closure = map f (F.lift' closure) :=
by
rw [map_lift'_eq2 (monotone_closure Y), map_lift'_eq (monotone_closure X)]
congr 1
ext s : 1
exact f_closed.closure_image_eq_of_continuous f_cont s
