English
For any u, t.restrictPreimage f restricted preimage equals the preimage under the composite map (a↦f a) of the image under Subtype.val of u.
Русский
Для любого u предобраз ограничения равен предобразу по композиции (a↦f a) от образа Subtype.val(u).
LaTeX
$$$t.\restrictPreimage f^{-1} u = (\lambda a: f a)^{-1}(\operatorname{image}(\operatorname{Subtype.val}, u))$$$
Lean4
theorem preimage_restrictPreimage {u : Set t} :
t.restrictPreimage f ⁻¹' u = (fun a : f ⁻¹' t ↦ f a) ⁻¹' (Subtype.val '' u) := by
rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
preimage_image_eq _ Subtype.val_injective]