symm_image_eq_source_inter_preimage

English

The inverse map images of a subset equal the source intersect the preimage under the forward map.

Русский

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

LaTeX

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

Lean4

theorem symm_image_eq_source_inter_preimage {s : Set Y} (h : s ⊆ e.target) : e.symm '' s = e.source ∩ e ⁻¹' s :=
  e.symm.image_eq_target_inter_inv_preimage h

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