English
The image under the projection val of the preimage of a set u under t.restrictPreimage f equals the preimage under f of the image of u under val.
Русский
Образ по проекции вал от предобраза множества u через t.restrictPreimage f равен предобразу по f от образа u через вал.
LaTeX
$$$\operatorname{image}(\operatorname{Subtype.val}, (t.\restrictPreimage f)\,^{-1}(u)) = f^{-1}(\operatorname{image}(\operatorname{Subtype.val}, u))$$$
Lean4
theorem image_val_preimage_restrictPreimage {u : Set t} :
Subtype.val '' (t.restrictPreimage f ⁻¹' u) = f ⁻¹' (Subtype.val '' u) :=
by
ext
simp