source_inter_preimage_inv_preimage

English

The source intersect with the preimage of the inverse image equals the source intersect the original set.

Русский

Источник пересекается с предобразом обратного образа равняется источнику пересечению с исходным множеством.

LaTeX

$$$e.source \cap e^{-1}(e^{-1}(s)) = e.source \cap s$$$

Lean4

theorem source_inter_preimage_inv_preimage (s : Set X) : e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
  e.toPartialEquiv.source_inter_preimage_inv_preimage s

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