target_subset_preimage_source — Mathlib

English

Restricting a partial equivalence to e.source ∩ s yields a new partial equivalence with the same action on its domain.

Русский

Ограничение частичного эквивалента до e.source ∩ s даёт новый частичный эквивалент, сохраняющий действие на своей области определения.

LaTeX

$$$(e.restr\\ s) : \\mathrm{PartialEquiv}(\\alpha,\\beta)$ is a restriction of e to e.source ∩ s with the same mapping.$$

Lean4

theorem target_subset_preimage_source : e.target ⊆ e.symm ⁻¹' e.source :=
  e.symm_mapsTo

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