English
There is a copy operation: given f and a new function f' equal to f, one can form f'.copy(f',h) which is again a pseudo-epimorphism α→β.
Русский
Существуют копии псевдоэпиморфизма: дано f и новая функция f' равная f, тогда f'.copy(f',h) снова является псевдоэпиморфизмом α→β.
LaTeX
$$$\mathrm{copy}:\mathrm{PseudoEpimorphism}(\alpha,\beta)\times(\alpha\to\beta)\to (f'=f)\to \mathrm{PseudoEpimorphism}(\alpha,\beta)$$$
Lean4
/-- Copy of a `PseudoEpimorphism` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = f) : PseudoEpimorphism α β :=
⟨f.toOrderHom.copy f' h, by simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'⟩
