English
A push-pull identity for maps and infimum: map f (F ⊓ comap f G) = map f F ⊓ G.
Русский
Идентичность push-pull для отображения и инфимума: map f (F ⊓ comap f G) = map f F ⊓ G.
LaTeX
$$protected theorem push_pull (f : α → β) (F : Filter α) (G : Filter β) : map f (F ⊓ comap f G) = map f F ⊓ G$$
Lean4
protected theorem push_pull (f : α → β) (F : Filter α) (G : Filter β) : map f (F ⊓ comap f G) = map f F ⊓ G :=
by
apply le_antisymm
·
calc
map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
_ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le
· rintro U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩
apply mem_inf_of_inter (image_mem_map V_in) Z_in
calc
f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
_ ⊆ f '' (V ∩ W) := by gcongr
_ = f '' (f ⁻¹' U) := by rw [h]
_ ⊆ U := image_preimage_subset f U
