image_val_preimage_restrictPreimage

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

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