preimage_restrictPreimage — Mathlib

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]

Похожие утверждения