English
Let e be a partial equivalence between α and β. If f equals e.toFun, g equals e.symm.toFun, s equals e.source, t equals e.target, and the related equalities hold, then the copy e.copy f hf g hg s hs t ht is exactly e. In other words, copying with the original data yields the original partial equivalence.
Русский
Пусть e — частичное эквив между α и β. Если f совпадает с e.toFun, g совпадает с e.symm.toFun, s совпадает с e.source, t совпадает с e.target и выполняются соответствующие равенства, то копия e.copy f hf g hg s hs t ht равна e. Иными словами, копирование с исходными данными возвращает исходное частичное эквив.
LaTeX
$$$e.copy\, f\, hf\, g\, hg\, s\, hs\, t\, ht = e$$$
Lean4
/-- Create a copy of a `PartialEquiv` providing better definitional equalities. -/
@[simps -fullyApplied]
def copy (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α) (hs : e.source = s)
(t : Set β) (ht : e.target = t) : PartialEquiv α β
where
toFun := f
invFun := g
source := s
target := t
map_source' _ := ht ▸ hs ▸ hf ▸ e.map_source
map_target' _ := hs ▸ ht ▸ hg ▸ e.map_target
left_inv' _ := hs ▸ hf ▸ hg ▸ e.left_inv
right_inv' _ := ht ▸ hf ▸ hg ▸ e.right_inv
