symm_image_target_inter_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem symm_image_target_inter_eq (s : Set β) : e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' (e.target ∩ s) :=
  e.symm.image_source_inter_eq _

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