source_inter_preimage_target_inter

English

Equality of image of intersection with source and intersection with target after preimage.

Русский

Равенство образа пересечения с источником и пересечения с целью после предобраза.

LaTeX

$$$e.toPartialEquiv.image_source_inter_eq s$$$

Lean4

theorem source_inter_preimage_target_inter (s : Set Y) : e.source ∩ e ⁻¹' (e.target ∩ s) = e.source ∩ e ⁻¹' s :=
  e.toPartialEquiv.source_inter_preimage_target_inter s

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