image_eq_target_inter_inv_preimage

English

If e maps s⊆e.source then e''s image on s equals e.target ∩ preimage of s under e.symm.

Русский

Если s ⊆ e.source, то образ e на s равен целевой части пересеченной с предобразом s по e.symm.

LaTeX

$$$\\forall e:\\mathrm{PartialEquiv}(\\alpha,\\beta),\\; s\\subseteq e.source\\Rightarrow e''s = e.target \\cap e.symm^{-1}(s)$$$

Lean4

theorem image_eq_target_inter_inv_preimage {s : Set α} (h : s ⊆ e.source) : e '' s = e.target ∩ e.symm ⁻¹' s := by
  rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]

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