English
Relating the image under the val map of a restricted preimage to the preimage under f of the image under val, one has a discrete equality of sets tying preimages and images together.
Русский
Связь образа по функции вала с предобразом по f от образа через вал устанавливает равенство множеств, связывающее предобраз и образ.
LaTeX
$$$\operatorname{image}( \operatorname{Subtype.val}, \; (t.\restrictionPreimage f)\, ) = \operatorname{preimage}( \operatorname{Subtype.val}, \operatorname{image}(f, s) )$$$
Lean4
theorem image_restrictPreimage : t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s) :=
by
delta Set.restrictPreimage
rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes, image_comp,
Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
