English
Copying an Esakia morphism with a new underlying function yields a valid Esakia morphism; the copy object preserves a prescribed equality of underlying maps.
Русский
Копирование морфизма Эзякия с новой базовой функцией образует допустимый морфизм Эзякия; копия сохраняет заданное равенство базовых отображений.
LaTeX
$$$\\text{copy}(f,f',h):= \\text{EsakiaHom}(\\,f',h\\,)$$$
Lean4
/-- Copy of an `EsakiaHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : EsakiaHom α β) (f' : α → β) (h : f' = f) : EsakiaHom α β :=
⟨f.toContinuousOrderHom.copy f' h, by simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'⟩
