image_source_inter_eq' — Mathlib

English

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

Русский

Образ e на e.source ∩ s равен e.target ∩ предобразу s по e.symm.

LaTeX

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

Lean4

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

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