English
The infimum of two filters under map composed with comap satisfies: map m (comap m f) = f ⊓ 𝓟(range m).
Русский
Перемещение через отображение и обратное изображение сохраняет инфимум: map m (comap m f) = f ⊓ 𝓟(range m).
LaTeX
$$$ \\operatorname{map}_m(\\operatorname{comap}_m f) = f \\;\\inf\\; \\mathcal{P}(\\operatorname{range}(m)) $$$
Lean4
theorem map_comap (f : Filter β) (m : α → β) : (f.comap m).map m = f ⊓ 𝓟 (range m) :=
by
refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_
rintro t' ⟨t, ht, sub⟩
refine mem_inf_principal.2 (mem_of_superset ht ?_)
rintro _ hxt ⟨x, rfl⟩
exact sub hxt
