English
Let e be a partial equivalence between α and β, and let s be a subset of β. Then composing e with the restriction of the identity on β to s yields the restriction of e to the subset e.source ∩ e^{-1}(s).
Русский
Пусть e — частичная эквивалентность между α и β, и пусть s ⊆ β. Тогда композиция e с ограничением идентичности на β до s равна ограничению e на подпространстве e.source ∩ e^{-1}(s).
LaTeX
$$$ e \\trans ((\\mathrm{refl} \\ β).restr_s) = e.restr (e.source \\cap e^{-1}(s)) $$$
Lean4
theorem trans_refl_restr' (s : Set β) : e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s) :=
PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) <|
by
simp only [trans_source, restr_source, refl_source, univ_inter]
rw [← inter_assoc, inter_self]
