English
Let f: α → β be a function and let F be a filter on α, G a filter on β. Then the push-forward of the infimum of comap f G and F equals the infimum of G and the push-forward of F: map f (comap f G ⊓ F) = G ⊓ map f F.
Русский
Пусть f: α → β и есть фильтры F на α и G на β. Тогда образ по f от пересечения comap f G и F равен пересечению G и образа по f от F: map f (comap f G ⊓ F) = G ⊓ map f F.
LaTeX
$$$ \operatorname{map} f (\operatorname{comap} f G \\inf F) = G \\inf \operatorname{map} f F $$$
Lean4
protected theorem push_pull' (f : α → β) (F : Filter α) (G : Filter β) : map f (comap f G ⊓ F) = G ⊓ map f F := by
simp only [Filter.push_pull, inf_comm]
