English
For injective f and a compatible g, there is an equality of filters: map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l).
Русский
Для инъективного f и согласованной g существует равенство фильтров: map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l).
LaTeX
$$$${\operatorname{map}(\Sigma.mk a)(\operatorname{comap}(g a) l)=\operatorname{comap}(\Sigma.map f g)(\operatorname{map}(\Sigma.mk (f a)) l)}$$$$
Lean4
theorem map_sigma_mk_comap {π : α → Type*} {π' : β → Type*} {f : α → β} (hf : Function.Injective f)
(g : ∀ a, π a → π' (f a)) (a : α) (l : Filter (π' (f a))) :
map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l) :=
by
refine (((basis_sets _).comap _).map _).eq_of_same_basis ?_
convert ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
apply image_sigmaMk_preimage_sigmaMap hf
