image_source_inter_eq — Mathlib

English

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

Русский

Образ e на e.source ∩ s равен целевой части пересечения с предобразом (e.source ∩ s) по e.symm.

LaTeX

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

Lean4

theorem image_source_inter_eq (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' (e.source ∩ s) := by
  rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]

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