English
There is a copy operation that produces a new bounded-order homomorphism from an old one by specifying a new underlying function equal to the old one; this is a tool to fix definitional equalities.
Русский
Существует операция копирования, которая порождает новый гомоморфизм ограниченного порядка на основе существующего, с заданной новой функцией, равной исходной; это средство для фиксации дефинитонных равенств.
LaTeX
$$$\text{Copy of } f: \alpha \to \beta$ is a bounded-order-homomorphism whose underlying function is a specified $f'$, with $f' = f$.$$
Lean4
/-- Copy of a `BoundedOrderHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : BoundedOrderHom α β) (f' : α → β) (h : f' = f) : BoundedOrderHom α β :=
{ f.toOrderHom.copy f' h, f.toTopHom.copy f' h, f.toBotHom.copy f' h with }
