symm_image_eq_source_inter_preimage

English

The symmetric image of e on e.target ∩ s equals e.source ∩ preimage of (e.target ∩ s) under e.

Русский

Симметрическое изображение e на e.target ∩ s равно e.source ∩ предобразу (e.target ∩ s) по e.

LaTeX

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

Lean4

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

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