image_source_inter_eq' — Mathlib

English

Equality of image of intersection with source and a corresponding intersection with target via inverse.

Русский

Равенство образа пересечения с источником и соответствующего пересечения через образ обратного отображения.

LaTeX

$$$\mathrm{image}(e.toFun')(e\text{.source} \cap s) = e.target \cap \mathrm{preimage}(e.symm.toFun', s)$$$

Lean4

theorem image_source_inter_eq' (s : Set X) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s :=
  e.toPartialEquiv.image_source_inter_eq' s

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